ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>f : Filter α<VAR>hf : Cauchy f<VAR>U : ℕ → Set (α × α)<VAR>U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α<VAR>U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s<VAR>a : α<VAR>ha : Filter.Tendsto (SequentiallyComplete.seq hf U_mem) Filter.atTop (𝓝 a)<GOAL>f ≤ 𝓝 a
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>(𝓤 α).IsCountablyGenerated<VAR>U : ℕ → Set (α × α)<VAR>U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α<VAR>HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Filter.Tendsto u Filter.atTop (𝓝 a)<GOAL>CompleteSpace α
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>(𝓤 α).IsCountablyGenerated<VAR>H' : ∀ (u : ℕ → α), CauchySeq u → ∃ a, Filter.Tendsto u Filter.atTop (𝓝 a)<GOAL>CompleteSpace α
<VAR>α : Type u<VAR>uniformSpace : UniformSpace α<VAR>(𝓤 α).IsCountablyGenerated<VAR>TopologicalSpace.SeparableSpace α<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<GOAL>LipschitzWith K f ↔ ∀ (x y : α), dist (f x) (f y) ≤ ↑K * dist x y
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<GOAL>LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>K : ℝ<VAR>h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y<GOAL>LipschitzWith K.toNNReal f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>h : ∀ (x y : α), dist (f x) (f y) ≤ dist x y<GOAL>LipschitzWith 1 f
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>f : α → ℝ<VAR>K : ℝ<VAR>h : ∀ (x y : α), f x ≤ f y + K * dist x y<GOAL>LipschitzWith K.toNNReal f
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>f : α → ℝ<VAR>K : ℝ≥0<VAR>h : ∀ (x y : α), f x ≤ f y + ↑K * dist x y<GOAL>LipschitzWith K f
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>f : α → ℝ<VAR>h : ∀ (x y : α), f x ≤ f y + dist x y<GOAL>LipschitzWith 1 f
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>f : α → ℝ<VAR>K : ℝ≥0<VAR>h : LipschitzWith K f<VAR>x y : α<GOAL>f x ≤ f y + ↑K * dist x y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>f : α → ℝ<VAR>K : ℝ≥0<GOAL>LipschitzWith K f ↔ ∀ (x y : α), f x ≤ f y + ↑K * dist x y
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : LipschitzWith K f<VAR>x y : α<GOAL>nndist (f x) (f y) ≤ K * nndist x y
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x y : α<VAR>r : ℝ<VAR>hf : LipschitzWith K f<VAR>hr : dist x y ≤ r<GOAL>dist (f x) (f y) ≤ ↑K * r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : LipschitzWith K f<VAR>x : α<VAR>r : ℝ<GOAL>Set.MapsTo f (Metric.closedBall x r) (Metric.closedBall (f x) (↑K * r))
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x y : α<VAR>r : ℝ<VAR>hf : LipschitzWith K f<VAR>hK : K ≠ 0<VAR>hr : dist x y < r<GOAL>dist (f x) (f y) < ↑K * r
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : LipschitzWith K f<VAR>hK : K ≠ 0<VAR>x : α<VAR>r : ℝ<GOAL>Set.MapsTo f (Metric.ball x r) (Metric.ball (f x) (↑K * r))
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : LipschitzWith K f<GOAL>⇑(LipschitzWith.toLocallyBoundedMap f hf) = f
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : LipschitzWith K f<GOAL>Filter.comap f (Bornology.cobounded β) ≤ Bornology.cobounded α
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : LipschitzWith K f<VAR>s : Set α<VAR>hs : Bornology.IsBounded s<GOAL>Bornology.IsBounded (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : LipschitzWith K f<VAR>s : Set α<VAR>hs : Bornology.IsBounded s<GOAL>Metric.diam (f '' s) ≤ ↑K * Metric.diam s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>y : α<GOAL>LipschitzWith 1 fun x => dist x y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>x : α<GOAL>LipschitzWith 1 (dist x)
<VAR>α : Type u<VAR>PseudoMetricSpace α<GOAL>LipschitzWith 2 (Function.uncurry dist)
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : LipschitzWith K f<VAR>x : α<VAR>n : ℕ<GOAL>dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * ↑K ^ n
<GOAL>LipschitzWith 1 fun p => max p.1 p.2
<GOAL>LipschitzWith 1 fun p => min p.1 p.2
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : LipschitzWith K f<VAR>u : ℕ → α<VAR>hu : CauchySeq u<GOAL>CauchySeq (f ∘ u)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f g : α → ℝ<VAR>Kf Kg : ℝ≥0<VAR>hf : LipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<GOAL>LipschitzWith (max Kf Kg) fun x => max (f x) (g x)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f g : α → ℝ<VAR>Kf Kg : ℝ≥0<VAR>hf : LipschitzWith Kf f<VAR>hg : LipschitzWith Kg g<GOAL>LipschitzWith (max Kf Kg) fun x => min (f x) (g x)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f : α → ℝ<VAR>Kf : ℝ≥0<VAR>hf : LipschitzWith Kf f<VAR>a : ℝ<GOAL>LipschitzWith Kf fun x => max (f x) a
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f : α → ℝ<VAR>Kf : ℝ≥0<VAR>hf : LipschitzWith Kf f<VAR>a : ℝ<GOAL>LipschitzWith Kf fun x => max a (f x)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f : α → ℝ<VAR>Kf : ℝ≥0<VAR>hf : LipschitzWith Kf f<VAR>a : ℝ<GOAL>LipschitzWith Kf fun x => min (f x) a
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f : α → ℝ<VAR>Kf : ℝ≥0<VAR>hf : LipschitzWith Kf f<VAR>a : ℝ<GOAL>LipschitzWith Kf fun x => min a (f x)
<VAR>a b : ℝ<VAR>h : a ≤ b<GOAL>LipschitzWith 1 (Set.projIcc a b h)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>s : Set α<VAR>f : α → β<VAR>K : ℝ<VAR>h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y<GOAL>LipschitzOnWith K.toNNReal f s
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>s : Set α<VAR>f : α → β<VAR>h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ dist x y<GOAL>LipschitzOnWith 1 f s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>f : α → ℝ<VAR>K : ℝ<VAR>h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y<GOAL>LipschitzOnWith K.toNNReal f s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>f : α → ℝ<VAR>K : ℝ≥0<VAR>h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + ↑K * dist x y<GOAL>LipschitzOnWith K f s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>f : α → ℝ<VAR>h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + dist x y<GOAL>LipschitzOnWith 1 f s
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>f : α → ℝ<VAR>K : ℝ≥0<VAR>h : LipschitzOnWith K f s<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<GOAL>f x ≤ f y + ↑K * dist x y
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>s : Set α<VAR>f : α → ℝ<VAR>K : ℝ≥0<GOAL>LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + ↑K * dist x y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>PseudoMetricSpace γ<VAR>f : α → β → γ<VAR>K₁ K₂ : ℝ≥0<VAR>s : Set α<VAR>t : Set β<VAR>hs : Bornology.IsBounded s<VAR>ht : Bornology.IsBounded t<VAR>hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun a => f a b) s<VAR>hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t<GOAL>Bornology.IsBounded (Set.image2 f s t)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>s : Set α<VAR>f : α → β<VAR>hf : LipschitzOnWith K f s<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>h'u : Set.range u ⊆ s<GOAL>CauchySeq (f ∘ u)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f g : α → ℝ<VAR>hf : LocallyLipschitz f<VAR>hg : LocallyLipschitz g<GOAL>LocallyLipschitz fun x => min (f x) (g x)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f g : α → ℝ<VAR>hf : LocallyLipschitz f<VAR>hg : LocallyLipschitz g<GOAL>LocallyLipschitz fun x => max (f x) (g x)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f : α → ℝ<VAR>hf : LocallyLipschitz f<VAR>a : ℝ<GOAL>LocallyLipschitz fun x => max (f x) a
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f : α → ℝ<VAR>hf : LocallyLipschitz f<VAR>a : ℝ<GOAL>LocallyLipschitz fun x => max a (f x)
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f : α → ℝ<VAR>hf : LocallyLipschitz f<VAR>a : ℝ<GOAL>LocallyLipschitz fun x => min (f x) a
<VAR>α : Type u<VAR>PseudoEMetricSpace α<VAR>f : α → ℝ<VAR>hf : LocallyLipschitz f<VAR>a : ℝ<GOAL>LocallyLipschitz fun x => min a (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>PseudoMetricSpace α<VAR>PseudoMetricSpace β<VAR>f : α → β<VAR>x : α<VAR>r : ℝ<VAR>hr : 0 < r<VAR>K : ℝ<VAR>h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x<GOAL>ContinuousAt f x
<VAR>α : Type u<VAR>PseudoMetricSpace α<VAR>f : α → ℝ<VAR>s : Set α<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<GOAL>∃ g, LipschitzWith K g ∧ Set.EqOn f g s
<VAR>α : Type u<VAR>ι : Type x<VAR>PseudoMetricSpace α<VAR>Fintype ι<VAR>f : α → ι → ℝ<VAR>s : Set α<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<GOAL>∃ g, LipschitzWith K g ∧ Set.EqOn f g s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>x : X<GOAL>∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, ∀ (i : ι), p.2 ∈ K i → EMetric.closedBall p.2 p.1 ⊆ U i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<VAR>x : X<GOAL>∃ r, ∀ᶠ (y : X) in 𝓝 x, r ∈ Set.Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ i, ⋂ (_ : y ∈ K i), {r | EMetric.closedBall y r ⊆ U i}
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>K U : ι → Set X<VAR>y : X<GOAL>Convex ℝ (Set.Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ i, ⋂ (_ : y ∈ K i), {r | EMetric.closedBall y r ⊆ U i})
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<GOAL>∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x (ENNReal.ofReal (δ x)) ⊆ U i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<GOAL>∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x ↑(δ x) ⊆ U i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>EMetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<GOAL>∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x (δ x) ⊆ U i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>MetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<GOAL>∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedBall x ↑(δ x) ⊆ U i
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>MetricSpace X<VAR>K U : ι → Set X<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<GOAL>∃ δ, (∀ (x : X), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedBall x (δ x) ⊆ U i
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>p' : Filter α<GOAL>TendstoUniformlyOnFilter F f p p' ↔ Filter.Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ p') (𝓤 β)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<GOAL>TendstoUniformlyOn F f p s ↔ TendstoUniformlyOnFilter F f p (𝓟 s)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>s : Set α<GOAL>TendstoUniformlyOn F f p s ↔ Filter.Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<GOAL>TendstoUniformlyOn F f p Set.univ ↔ TendstoUniformly F f p
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<GOAL>TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>h : TendstoUniformly F f p<GOAL>TendstoUniformlyOnFilter F f p ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<GOAL>TendstoUniformlyOn F f p s ↔ TendstoUniformly (fun i x => F i ↑x) (f ∘ Subtype.val) p
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<GOAL>TendstoUniformly F f p ↔ Filter.Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ ⊤) (𝓤 β)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>h : TendstoUniformlyOnFilter F f p p'<VAR>hx : 𝓟 {x} ≤ p'<GOAL>Filter.Tendsto (fun n => F n x) p (𝓝 (f x))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>h : TendstoUniformlyOn F f p s<VAR>x : α<VAR>hx : x ∈ s<GOAL>Filter.Tendsto (fun n => F n x) p (𝓝 (f x))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>h : TendstoUniformly F f p<VAR>x : α<GOAL>Filter.Tendsto (fun n => F n x) p (𝓝 (f x))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>p' : Filter α<VAR>p'' : Filter ι<VAR>h : TendstoUniformlyOnFilter F f p p'<VAR>hp : p'' ≤ p<GOAL>TendstoUniformlyOnFilter F f p'' p'
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>p' p'' : Filter α<VAR>h : TendstoUniformlyOnFilter F f p p'<VAR>hp : p'' ≤ p'<GOAL>TendstoUniformlyOnFilter F f p p''
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>s' : Set α<VAR>h : TendstoUniformlyOn F f p s<VAR>h' : s' ⊆ s<GOAL>TendstoUniformlyOn F f p s'
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>p' : Filter α<VAR>F' : ι → α → β<VAR>hf : TendstoUniformlyOnFilter F f p p'<VAR>hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.1 n.2 = F' n.1 n.2<GOAL>TendstoUniformlyOnFilter F' f p p'
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>F' : ι → α → β<VAR>hf : TendstoUniformlyOn F f p s<VAR>hff' : ∀ᶠ (n : ι) in p, Set.EqOn (F n) (F' n) s<GOAL>TendstoUniformlyOn F' f p s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>g : α → β<VAR>hf : TendstoUniformlyOn F f p s<VAR>hfg : Set.EqOn f g s<GOAL>TendstoUniformlyOn F g p s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>h : TendstoUniformly F f p<GOAL>TendstoUniformlyOn F f p s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>p' : Filter α<VAR>h : TendstoUniformlyOnFilter F f p p'<VAR>g : γ → α<GOAL>TendstoUniformlyOnFilter (fun n => F n ∘ g) (f ∘ g) p (Filter.comap g p')
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>h : TendstoUniformlyOn F f p s<VAR>g : γ → α<GOAL>TendstoUniformlyOn (fun n => F n ∘ g) (f ∘ g) p (g ⁻¹' s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>h : TendstoUniformly F f p<VAR>g : γ → α<GOAL>TendstoUniformly (fun n => F n ∘ g) (f ∘ g) p
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>p' : Filter α<VAR>UniformSpace γ<VAR>g : β → γ<VAR>hg : UniformContinuous g<VAR>h : TendstoUniformlyOnFilter F f p p'<GOAL>TendstoUniformlyOnFilter (fun i => g ∘ F i) (g ∘ f) p p'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>UniformSpace γ<VAR>g : β → γ<VAR>hg : UniformContinuous g<VAR>h : TendstoUniformlyOn F f p s<GOAL>TendstoUniformlyOn (fun i => g ∘ F i) (g ∘ f) p s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>UniformSpace γ<VAR>g : β → γ<VAR>hg : UniformContinuous g<VAR>h : TendstoUniformly F f p<GOAL>TendstoUniformly (fun i => g ∘ F i) (g ∘ f) p
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>p' : Filter α<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>f' : α' → β'<VAR>q : Filter ι'<VAR>q' : Filter α'<VAR>h : TendstoUniformlyOnFilter F f p p'<VAR>h' : TendstoUniformlyOnFilter F' f' q q'<GOAL>TendstoUniformlyOnFilter (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ q) (p' ×ˢ q')
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>f' : α' → β'<VAR>p' : Filter ι'<VAR>s' : Set α'<VAR>h : TendstoUniformlyOn F f p s<VAR>h' : TendstoUniformlyOn F' f' p' s'<GOAL>TendstoUniformlyOn (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (s ×ˢ s')
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>ι' : Type u_1<VAR>α' : Type u_2<VAR>β' : Type u_3<VAR>UniformSpace β'<VAR>F' : ι' → α' → β'<VAR>f' : α' → β'<VAR>p' : Filter ι'<VAR>h : TendstoUniformly F f p<VAR>h' : TendstoUniformly F' f' p'<GOAL>TendstoUniformly (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>p' : Filter α<VAR>ι' : Type u_1<VAR>β' : Type u_2<VAR>UniformSpace β'<VAR>F' : ι' → α → β'<VAR>f' : α → β'<VAR>q : Filter ι'<VAR>h : TendstoUniformlyOnFilter F f p p'<VAR>h' : TendstoUniformlyOnFilter F' f' q p'<GOAL>TendstoUniformlyOnFilter (fun i a => (F i.1 a, F' i.2 a)) (fun a => (f a, f' a)) (p ×ˢ q) p'
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>ι' : Type u_1<VAR>β' : Type u_2<VAR>UniformSpace β'<VAR>F' : ι' → α → β'<VAR>f' : α → β'<VAR>p' : Filter ι'<VAR>h : TendstoUniformlyOn F f p s<VAR>h' : TendstoUniformlyOn F' f' p' s<GOAL>TendstoUniformlyOn (fun i a => (F i.1 a, F' i.2 a)) (fun a => (f a, f' a)) (p.prod p') s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>ι' : Type u_1<VAR>β' : Type u_2<VAR>UniformSpace β'<VAR>F' : ι' → α → β'<VAR>f' : α → β'<VAR>p' : Filter ι'<VAR>h : TendstoUniformly F f p<VAR>h' : TendstoUniformly F' f' p'<GOAL>TendstoUniformly (fun i a => (F i.1 a, F' i.2 a)) (fun a => (f a, f' a)) (p ×ˢ p')
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>p : Filter ι<VAR>p' : Filter α<VAR>c : β<GOAL>Filter.Tendsto (↿F) (p ×ˢ p') (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun x => c) p p'
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>c : β<GOAL>Filter.Tendsto (↿F) (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOn F (fun x => c) p s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>p : Filter ι<VAR>c : β<GOAL>Filter.Tendsto (↿F) (p ×ˢ ⊤) (𝓝 c) ↔ TendstoUniformly F (fun x => c) p
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<GOAL>TendstoUniformlyOn F f p ∅
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>x : α<VAR>p : Filter ι<GOAL>TendstoUniformlyOn F f p {x} ↔ Filter.Tendsto (fun n => F n x) p (𝓝 (f x))
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>p : Filter ι<VAR>g : ι → β<VAR>b : β<VAR>hg : Filter.Tendsto g p (𝓝 b)<VAR>p' : Filter α<GOAL>TendstoUniformlyOnFilter (fun n x => g n) (fun x => b) p p'
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>p : Filter ι<VAR>g : ι → β<VAR>b : β<VAR>hg : Filter.Tendsto g p (𝓝 b)<VAR>s : Set α<GOAL>TendstoUniformlyOn (fun n x => g n) (fun x => b) p s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>UniformSpace β<VAR>UniformSpace α<VAR>UniformSpace γ<VAR>x : α<VAR>U : Set α<VAR>V : Set β<VAR>F : α → β → γ<VAR>hF : UniformContinuousOn (↿F) (U ×ˢ V)<VAR>hU : x ∈ U<GOAL>TendstoUniformlyOn F (F x) (𝓝[U] x) V
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>UniformSpace β<VAR>UniformSpace α<VAR>UniformSpace γ<VAR>x : α<VAR>U : Set α<VAR>hU : U ∈ 𝓝 x<VAR>F : α → β → γ<VAR>hF : UniformContinuousOn (↿F) (U ×ˢ Set.univ)<GOAL>TendstoUniformly F (F x) (𝓝 x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>UniformSpace β<VAR>UniformSpace α<VAR>UniformSpace γ<VAR>f : α → β → γ<VAR>h : UniformContinuous₂ f<VAR>x : α<GOAL>TendstoUniformly f (f x) (𝓝 x)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>s : Set α<VAR>p : Filter ι<GOAL>UniformCauchySeqOn F p s ↔ UniformCauchySeqOnFilter F p (𝓟 s)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>hF : UniformCauchySeqOn F p s<GOAL>UniformCauchySeqOnFilter F p (𝓟 s)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>p' : Filter α<VAR>hF : TendstoUniformlyOnFilter F f p p'<GOAL>UniformCauchySeqOnFilter F p p'
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>hF : TendstoUniformlyOn F f p s<GOAL>UniformCauchySeqOn F p s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>p : Filter ι<VAR>p' : Filter α<VAR>p.NeBot<VAR>hF : UniformCauchySeqOnFilter F p p'<VAR>hF' : ∀ᶠ (x : α) in p', Filter.Tendsto (fun n => F n x) p (𝓝 (f x))<GOAL>TendstoUniformlyOnFilter F f p p'
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>p.NeBot<VAR>hF : UniformCauchySeqOn F p s<VAR>hF' : ∀ x ∈ s, Filter.Tendsto (fun n => F n x) p (𝓝 (f x))<GOAL>TendstoUniformlyOn F f p s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>p : Filter ι<VAR>p' : Filter α<VAR>p'' : Filter ι<VAR>hf : UniformCauchySeqOnFilter F p p'<VAR>hp : p'' ≤ p<GOAL>UniformCauchySeqOnFilter F p'' p'
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>p : Filter ι<VAR>p' p'' : Filter α<VAR>hf : UniformCauchySeqOnFilter F p p'<VAR>hp : p'' ≤ p'<GOAL>UniformCauchySeqOnFilter F p p''
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>s' : Set α<VAR>hf : UniformCauchySeqOn F p s<VAR>hss' : s' ⊆ s<GOAL>UniformCauchySeqOn F p s'
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>p : Filter ι<VAR>p' : Filter α<VAR>γ : Type u_1<VAR>hf : UniformCauchySeqOnFilter F p p'<VAR>g : γ → α<GOAL>UniformCauchySeqOnFilter (fun n => F n ∘ g) p (Filter.comap g p')
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type x<VAR>UniformSpace β<VAR>F : ι → α → β<VAR>s : Set α<VAR>p : Filter ι<VAR>γ : Type u_1<VAR>hf : UniformCauchySeqOn F p s<VAR>g : γ → α<GOAL>UniformCauchySeqOn (fun n => F n ∘ g) p (g ⁻¹' s)