ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>p : κ → Prop<VAR>s : κ → Set X<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>hX : (nhdsWithin x₀ S).HasBasis p s<GOAL>EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ uniformity α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ (i : ι), (F i x₀, F i x) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>p : κ → Prop<VAR>s : κ → Set (α × α)<VAR>F : ι → X → α<VAR>x₀ : X<VAR>hα : (uniformity α).HasBasis p s<GOAL>EquicontinuousAt F x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in nhds x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>p : κ → Prop<VAR>s : κ → Set (α × α)<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>hα : (uniformity α).HasBasis p s<GOAL>EquicontinuousWithinAt F S x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in nhdsWithin x₀ S, ∀ (i : ι), (F i x₀, F i x) ∈ s k
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>κ₁ : Type u_13<VAR>κ₂ : Type u_14<VAR>p₁ : κ₁ → Prop<VAR>s₁ : κ₁ → Set X<VAR>p₂ : κ₂ → Prop<VAR>s₂ : κ₂ → Set (α × α)<VAR>F : ι → X → α<VAR>x₀ : X<VAR>hX : (nhds x₀).HasBasis p₁ s₁<VAR>hα : (uniformity α).HasBasis p₂ s₂<GOAL>EquicontinuousAt F x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>κ₁ : Type u_13<VAR>κ₂ : Type u_14<VAR>p₁ : κ₁ → Prop<VAR>s₁ : κ₁ → Set X<VAR>p₂ : κ₂ → Prop<VAR>s₂ : κ₂ → Set (α × α)<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>hX : (nhdsWithin x₀ S).HasBasis p₁ s₁<VAR>hα : (uniformity α).HasBasis p₂ s₂<GOAL>EquicontinuousWithinAt F S x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>p : κ → Prop<VAR>s : κ → Set (β × β)<VAR>F : ι → β → α<VAR>hβ : (uniformity β).HasBasis p s<GOAL>UniformEquicontinuous F ↔ ∀ U ∈ uniformity α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>p : κ → Prop<VAR>s : κ → Set (β × β)<VAR>F : ι → β → α<VAR>S : Set β<VAR>hβ : (uniformity β ⊓ Filter.principal (S ×ˢ S)).HasBasis p s<GOAL>UniformEquicontinuousOn F S ↔ ∀ U ∈ uniformity α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>p : κ → Prop<VAR>s : κ → Set (α × α)<VAR>F : ι → β → α<VAR>hα : (uniformity α).HasBasis p s<GOAL>UniformEquicontinuous F ↔ ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in uniformity β, ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>p : κ → Prop<VAR>s : κ → Set (α × α)<VAR>F : ι → β → α<VAR>S : Set β<VAR>hα : (uniformity α).HasBasis p s<GOAL>UniformEquicontinuousOn F S ↔ ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in uniformity β ⊓ Filter.principal (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) ∈ s k
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>κ₁ : Type u_13<VAR>κ₂ : Type u_14<VAR>p₁ : κ₁ → Prop<VAR>s₁ : κ₁ → Set (β × β)<VAR>p₂ : κ₂ → Prop<VAR>s₂ : κ₂ → Set (α × α)<VAR>F : ι → β → α<VAR>hβ : (uniformity β).HasBasis p₁ s₁<VAR>hα : (uniformity α).HasBasis p₂ s₂<GOAL>UniformEquicontinuous F ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>κ₁ : Type u_13<VAR>κ₂ : Type u_14<VAR>p₁ : κ₁ → Prop<VAR>s₁ : κ₁ → Set (β × β)<VAR>p₂ : κ₂ → Prop<VAR>s₂ : κ₂ → Set (α × α)<VAR>F : ι → β → α<VAR>S : Set β<VAR>hβ : (uniformity β ⊓ Filter.principal (S ×ˢ S)).HasBasis p₁ s₁<VAR>hα : (uniformity α).HasBasis p₂ s₂<GOAL>UniformEquicontinuousOn F S ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>β : Type u_9<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → X → α<VAR>x₀ : X<VAR>u : α → β<VAR>hu : UniformInducing u<GOAL>EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x => u ∘ x) ∘ F) x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>β : Type u_9<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>u : α → β<VAR>hu : UniformInducing u<GOAL>EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((fun x => u ∘ x) ∘ F) S x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>β : Type u_9<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → X → α<VAR>u : α → β<VAR>hu : UniformInducing u<GOAL>Equicontinuous F ↔ Equicontinuous ((fun x => u ∘ x) ∘ F)
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>β : Type u_9<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>F : ι → X → α<VAR>S : Set X<VAR>u : α → β<VAR>hu : UniformInducing u<GOAL>EquicontinuousOn F S ↔ EquicontinuousOn ((fun x => u ∘ x) ∘ F) S
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>γ : Type u_11<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → β → α<VAR>u : α → γ<VAR>hu : UniformInducing u<GOAL>UniformEquicontinuous F ↔ UniformEquicontinuous ((fun x => u ∘ x) ∘ F)
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>γ : Type u_11<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → β → α<VAR>S : Set β<VAR>u : α → γ<VAR>hu : UniformInducing u<GOAL>UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((fun x => u ∘ x) ∘ F) S
<VAR>X : Type u_3<VAR>Y : Type u_5<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>uα : UniformSpace α<VAR>A : Set Y<VAR>u : Y → X → α<VAR>S : Set X<VAR>x₀ : X<VAR>hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀<VAR>hu₁ : Continuous (S.restrict ∘ u)<VAR>hu₂ : Continuous (Function.eval x₀ ∘ u)<GOAL>EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
<VAR>X : Type u_3<VAR>Y : Type u_5<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>uα : UniformSpace α<VAR>A : Set Y<VAR>u : Y → X → α<VAR>x₀ : X<VAR>hA : EquicontinuousAt (u ∘ Subtype.val) x₀<VAR>hu : Continuous u<GOAL>EquicontinuousAt (u ∘ Subtype.val) x₀
<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>A : Set (X → α)<VAR>x₀ : X<VAR>hA : A.EquicontinuousAt x₀<GOAL>(closure A).EquicontinuousAt x₀
<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>A : Set (X → α)<VAR>S : Set X<VAR>x₀ : X<VAR>hA : A.EquicontinuousWithinAt S x₀<GOAL>(closure A).EquicontinuousWithinAt S x₀
<VAR>X : Type u_3<VAR>Y : Type u_5<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>uα : UniformSpace α<VAR>A : Set Y<VAR>u : Y → X → α<VAR>hA : Equicontinuous (u ∘ Subtype.val)<VAR>hu : Continuous u<GOAL>Equicontinuous (u ∘ Subtype.val)
<VAR>X : Type u_3<VAR>Y : Type u_5<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>uα : UniformSpace α<VAR>A : Set Y<VAR>u : Y → X → α<VAR>S : Set X<VAR>hA : EquicontinuousOn (u ∘ Subtype.val) S<VAR>hu : Continuous (S.restrict ∘ u)<GOAL>EquicontinuousOn (u ∘ Subtype.val) S
<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>A : Set (X → α)<VAR>hA : A.Equicontinuous<GOAL>(closure A).Equicontinuous
<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>A : Set (X → α)<VAR>S : Set X<VAR>hA : A.EquicontinuousOn S<GOAL>(closure A).EquicontinuousOn S
<VAR>Y : Type u_5<VAR>α : Type u_7<VAR>β : Type u_9<VAR>tY : TopologicalSpace Y<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>A : Set Y<VAR>u : Y → β → α<VAR>S : Set β<VAR>hA : UniformEquicontinuousOn (u ∘ Subtype.val) S<VAR>hu : Continuous (S.restrict ∘ u)<GOAL>UniformEquicontinuousOn (u ∘ Subtype.val) S
<VAR>Y : Type u_5<VAR>α : Type u_7<VAR>β : Type u_9<VAR>tY : TopologicalSpace Y<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>A : Set Y<VAR>u : Y → β → α<VAR>hA : UniformEquicontinuous (u ∘ Subtype.val)<VAR>hu : Continuous u<GOAL>UniformEquicontinuous (u ∘ Subtype.val)
<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>A : Set (β → α)<VAR>hA : A.UniformEquicontinuous<GOAL>(closure A).UniformEquicontinuous
<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>A : Set (β → α)<VAR>S : Set β<VAR>hA : A.UniformEquicontinuousOn S<GOAL>(closure A).UniformEquicontinuousOn S
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>l : Filter ι<VAR>l.NeBot<VAR>F : ι → X → α<VAR>f : X → α<VAR>S : Set X<VAR>x₀ : X<VAR>h₁ : ∀ x ∈ S, Filter.Tendsto (fun x_1 => F x_1 x) l (nhds (f x))<VAR>h₂ : Filter.Tendsto (fun x => F x x₀) l (nhds (f x₀))<VAR>h₃ : EquicontinuousWithinAt F S x₀<GOAL>ContinuousWithinAt f S x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>l : Filter ι<VAR>l.NeBot<VAR>F : ι → X → α<VAR>f : X → α<VAR>x₀ : X<VAR>h₁ : Filter.Tendsto F l (nhds f)<VAR>h₂ : EquicontinuousAt F x₀<GOAL>ContinuousAt f x₀
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>l : Filter ι<VAR>l.NeBot<VAR>F : ι → X → α<VAR>f : X → α<VAR>h₁ : Filter.Tendsto F l (nhds f)<VAR>h₂ : Equicontinuous F<GOAL>Continuous f
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>l : Filter ι<VAR>l.NeBot<VAR>F : ι → X → α<VAR>f : X → α<VAR>S : Set X<VAR>h₁ : ∀ x ∈ S, Filter.Tendsto (fun x_1 => F x_1 x) l (nhds (f x))<VAR>h₂ : EquicontinuousOn F S<GOAL>ContinuousOn f S
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>l : Filter ι<VAR>l.NeBot<VAR>F : ι → β → α<VAR>f : β → α<VAR>S : Set β<VAR>h₁ : ∀ x ∈ S, Filter.Tendsto (fun x_1 => F x_1 x) l (nhds (f x))<VAR>h₂ : UniformEquicontinuousOn F S<GOAL>UniformContinuousOn f S
<VAR>ι : Type u_1<VAR>α : Type u_7<VAR>β : Type u_9<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>l : Filter ι<VAR>l.NeBot<VAR>F : ι → β → α<VAR>f : β → α<VAR>h₁ : Filter.Tendsto F l (nhds f)<VAR>h₂ : UniformEquicontinuous F<GOAL>UniformContinuous f
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>l : Filter ι<VAR>F : ι → X → α<VAR>f : X → α<VAR>s : Set X<VAR>x : X<VAR>z : α<VAR>hF : EquicontinuousAt F x<VAR>hf : Filter.Tendsto f (nhdsWithin x s) (nhds z)<VAR>hs : ∀ y ∈ s, Filter.Tendsto (fun x => F x y) l (nhds (f y))<VAR>hx : x ∈ closure s<GOAL>Filter.Tendsto (fun x_1 => F x_1 x) l (nhds z)
<VAR>ι : Type u_1<VAR>X : Type u_3<VAR>α : Type u_7<VAR>tX : TopologicalSpace X<VAR>uα : UniformSpace α<VAR>l : Filter ι<VAR>F : ι → X → α<VAR>f : X → α<VAR>hF : Equicontinuous F<VAR>hf : Continuous f<GOAL>IsClosed {x | Filter.Tendsto (fun x_1 => F x_1 x) l (nhds (f x))}
<VAR>α : Type u<VAR>EMetricSpace α<GOAL>Continuous fun p => EMetric.infEdist p.1 ↑p.2
<VAR>α : Type u<VAR>EMetricSpace α<VAR>s : Set α<VAR>hs : IsClosed s<GOAL>IsClosed {t | ↑t ⊆ s}
<VAR>α : Type u<VAR>EMetricSpace α<VAR>s t : TopologicalSpace.Closeds α<GOAL>edist s t = EMetric.hausdorffEdist ↑s ↑t
<VAR>α : Type u<VAR>EMetricSpace α<GOAL>UniformEmbedding TopologicalSpace.NonemptyCompacts.toCloseds
<VAR>α : Type u<VAR>EMetricSpace α<VAR>CompleteSpace α<GOAL>IsClosed (Set.range TopologicalSpace.NonemptyCompacts.toCloseds)
<VAR>α : Type u<VAR>MetricSpace α<VAR>x y : TopologicalSpace.NonemptyCompacts α<GOAL>dist x y = Metric.hausdorffDist ↑x ↑y
<VAR>α : Type u<VAR>MetricSpace α<VAR>x : α<GOAL>LipschitzWith 1 fun s => Metric.infDist x ↑s
<VAR>α : Type u<VAR>MetricSpace α<GOAL>LipschitzWith 2 fun p => Metric.infDist p.1 ↑p.2
<VAR>α : Type u<VAR>MetricSpace α<GOAL>UniformContinuous fun p => Metric.infDist p.1 ↑p.2
<VAR>α : Type ua<VAR>a b : α<GOAL>(a, b) ∈ idRel ↔ a = b
<VAR>α : Type ua<VAR>s : Set (α × α)<GOAL>idRel ⊆ s ↔ ∀ (a : α), (a, a) ∈ s
<VAR>α : Type u<VAR>r₁ r₂ : Set (α × α)<VAR>x y : α<GOAL>(x, y) ∈ r₁ ○ r₂ ↔ ∃ z, (x, z) ∈ r₁ ∧ (z, y) ∈ r₂
<VAR>α : Type ua<GOAL>Prod.swap '' idRel = idRel
<VAR>α : Type ua<VAR>β : Type ub<VAR>Preorder β<VAR>f g : β → Set (α × α)<VAR>hf : Monotone f<VAR>hg : Monotone g<GOAL>Monotone fun x => f x ○ g x
<VAR>α : Type ua<VAR>f g h k : Set (α × α)<VAR>h₁ : f ⊆ h<VAR>h₂ : g ⊆ k<GOAL>f ○ g ⊆ h ○ k
<VAR>α : Type ua<VAR>a b c : α<VAR>s t : Set (α × α)<VAR>h₁ : (a, c) ∈ s<VAR>h₂ : (c, b) ∈ t<GOAL>(a, b) ∈ s ○ t
<VAR>α : Type ua<VAR>r : Set (α × α)<GOAL>idRel ○ r = r
<VAR>α : Type ua<VAR>r s t : Set (α × α)<GOAL>r ○ s ○ t = r ○ (s ○ t)
<VAR>α : Type ua<VAR>s t : Set (α × α)<VAR>h : idRel ⊆ t<GOAL>s ⊆ s ○ t
<VAR>α : Type ua<VAR>s t : Set (α × α)<VAR>h : idRel ⊆ s<GOAL>t ⊆ s ○ t
<VAR>α : Type ua<VAR>s : Set (α × α)<VAR>h : idRel ⊆ s<GOAL>s ⊆ s ○ s
<VAR>α : Type ua<VAR>s t : Set (α × α)<VAR>h : idRel ⊆ s<VAR>n : ℕ<GOAL>t ⊆ (fun x => s ○ x)^[n] t
<VAR>α : Type ua<VAR>V : Set (α × α)<GOAL>SymmetricRel (symmetrizeRel V)
<VAR>α : Type ua<VAR>V : Set (α × α)<GOAL>symmetrizeRel V ⊆ V
<VAR>α : Type ua<VAR>V W : Set (α × α)<VAR>h : V ⊆ W<GOAL>symmetrizeRel V ⊆ symmetrizeRel W
<VAR>α : Type ua<VAR>V : Set (α × α)<VAR>hV : SymmetricRel V<VAR>x y : α<GOAL>(x, y) ∈ V ↔ (y, x) ∈ V
<VAR>α : Type ua<VAR>U : Set (α × α)<VAR>hU : SymmetricRel U<GOAL>Prod.swap ⁻¹' U = U
<VAR>α : Type ua<VAR>U V : Set (α × α)<VAR>hU : SymmetricRel U<VAR>hV : SymmetricRel V<GOAL>SymmetricRel (U ∩ V)
<VAR>α : Type u<VAR>self : UniformSpace.Core α<GOAL>(self.uniformity.lift' fun s => s ○ s) ≤ self.uniformity
<VAR>α : Type u<VAR>self : UniformSpace.Core α<GOAL>Filter.Tendsto Prod.swap self.uniformity self.uniformity
<VAR>α : Type u<VAR>self : UniformSpace.Core α<GOAL>𝓟 idRel ≤ self.uniformity
<VAR>α : Type ua<VAR>c : UniformSpace.Core α<VAR>s : Set (α × α)<VAR>hs : s ∈ c.uniformity<GOAL>∃ t ∈ c.uniformity, t ○ t ⊆ s
<VAR>α : Type ua<VAR>u₁ u₂ : UniformSpace.Core α<GOAL>u₁.uniformity = u₂.uniformity → u₁ = u₂
<VAR>α : Type u<VAR>u : UniformSpace.Core α<VAR>x : α<GOAL>𝓝 x = Filter.comap (Prod.mk x) u.uniformity
<VAR>α : Type u<VAR>self : UniformSpace α<VAR>x : α<GOAL>𝓝 x = Filter.comap (Prod.mk x) UniformSpace.uniformity
<VAR>α : Type u<VAR>self : UniformSpace α<GOAL>Filter.Tendsto Prod.swap UniformSpace.uniformity UniformSpace.uniformity
<VAR>α : Type u<VAR>self : UniformSpace α<GOAL>(UniformSpace.uniformity.lift' fun s => s ○ s) ≤ UniformSpace.uniformity
<VAR>α : Type ua<VAR>u : UniformSpace α<GOAL>u.toCore.toTopologicalSpace = UniformSpace.toTopologicalSpace
<VAR>α : Type ua<VAR>u₁ u₂ : UniformSpace α<VAR>h : 𝓤 α = 𝓤 α<GOAL>u₁ = u₂
<VAR>α : Type ua<VAR>u₁ u₂ : UniformSpace α<GOAL>u₁ = u₂ ↔ ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α
<VAR>α : Type ua<VAR>u : UniformSpace α<VAR>t : TopologicalSpace α<VAR>h : t = u.toCore.toTopologicalSpace<GOAL>UniformSpace.ofCoreEq u.toCore t h = u
<VAR>α : Type u_2<VAR>i : TopologicalSpace α<VAR>u : UniformSpace α<VAR>h : i = UniformSpace.toTopologicalSpace<GOAL>u.replaceTopology h = u
<VAR>α : Type u<VAR>β : Type v<VAR>LinearOrderedAddCommMonoid β<VAR>h₀ : ∃ x, 0 < x<VAR>d : α → α → β<VAR>refl : ∀ (x : α), d x x = 0<VAR>symm : ∀ (x y : α), d x y = d y x<VAR>triangle : ∀ (x y z : α), d x z ≤ d x y + d y z<VAR>half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε<GOAL>(𝓤 α).HasBasis (fun x => 0 < x) fun ε => {x | d x.1 x.2 < ε}
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<GOAL>𝓝 x = Filter.comap (Prod.mk x) (𝓤 α)
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set α<GOAL>IsOpen s ↔ ∀ x ∈ s, {p | p.1 = x → p.2 ∈ s} ∈ 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>𝓟 idRel ≤ 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<VAR>s : Set (α × α)<VAR>h : s ∈ 𝓤 α<GOAL>(x, x) ∈ s
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x y : α<VAR>s : Set (α × α)<VAR>h : s ∈ 𝓤 α<VAR>hx : x = y<GOAL>(x, y) ∈ s
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>Filter.map Prod.swap (𝓤 α) ≤ 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>((𝓤 α).lift' fun s => s ○ s) ≤ 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>((𝓤 α).lift' fun s => s ○ s) = 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>Filter.Tendsto Prod.swap (𝓤 α) (𝓤 α)
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>∃ t ∈ 𝓤 α, t ○ t ⊆ s
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>n : ℕ<GOAL>∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, (fun x => t ○ x)^[n] t ⊆ s
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>∀ᶠ (t : Set (α × α)) in (𝓤 α).smallSets, t ○ t ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>l : Filter β<VAR>f₁ f₂ f₃ : β → α<VAR>h₁₂ : Filter.Tendsto (fun x => (f₁ x, f₂ x)) l (𝓤 α)<VAR>h₂₃ : Filter.Tendsto (fun x => (f₂ x, f₃ x)) l (𝓤 α)<GOAL>Filter.Tendsto (fun x => (f₁ x, f₃ x)) l (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>l : Filter β<VAR>f : β → α × α<VAR>h : Filter.Tendsto f l (𝓤 α)<GOAL>Filter.Tendsto (fun x => ((f x).2, (f x).1)) l (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>f : β → α<VAR>l : Filter β<GOAL>Filter.Tendsto (fun x => (f x, f x)) l (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>a : α<VAR>f : Filter β<GOAL>Filter.Tendsto (fun x => (a, a)) f (𝓤 α)
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>∃ t ∈ 𝓤 α, (∀ (a b : α), (a, b) ∈ t → (b, a) ∈ t) ∧ t ⊆ s
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>∃ t ∈ 𝓤 α, (∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t) ∧ t ○ t ⊆ s
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>𝓤 α ≤ Prod.swap <$> 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>𝓤 α = Prod.swap <$> 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>Filter.comap Prod.swap (𝓤 α) = 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<VAR>V : Set (α × α)<VAR>h : V ∈ 𝓤 α<GOAL>symmetrizeRel V ∈ 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>(𝓤 α).HasBasis (fun s => s ∈ 𝓤 α ∧ SymmetricRel s) id
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>g : Set (α × α) → Filter β<VAR>f : Filter β<VAR>hg : Monotone g<VAR>h : ((𝓤 α).lift fun s => g (Prod.swap ⁻¹' s)) ≤ f<GOAL>(𝓤 α).lift g ≤ f
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>f : Set (α × α) → Filter β<VAR>h : Monotone f<GOAL>((𝓤 α).lift fun s => f (s ○ s)) ≤ (𝓤 α).lift f
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>∃ t ∈ 𝓤 α, t ○ (t ○ t) ⊆ s
<VAR>α : Type ua<VAR>UniformSpace α<GOAL>((𝓤 α).lift' fun s => s ○ (s ○ s)) ≤ 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ⊆ s
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set (α × α)<VAR>h : s ∈ 𝓤 α<GOAL>s ⊆ s ○ s
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>∃ t ∈ 𝓤 α, SymmetricRel t ∧ t ○ t ○ t ⊆ s
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<VAR>V : Set (α × α)<VAR>hV : V ∈ 𝓤 α<GOAL>x ∈ UniformSpace.ball x V
<VAR>β : Type ub<VAR>V W : Set (β × β)<VAR>x y z : β<VAR>h : y ∈ UniformSpace.ball x V<VAR>h' : z ∈ UniformSpace.ball y W<GOAL>z ∈ UniformSpace.ball x (V ○ W)
<VAR>β : Type ub<VAR>V W : Set (β × β)<VAR>x y : β<VAR>h : x ∈ UniformSpace.ball y W<VAR>h' : W ○ W ⊆ V<GOAL>UniformSpace.ball x W ⊆ UniformSpace.ball y V
<VAR>β : Type ub<VAR>V W : Set (β × β)<VAR>h : V ⊆ W<VAR>x : β<GOAL>UniformSpace.ball x V ⊆ UniformSpace.ball x W
<VAR>β : Type ub<VAR>x : β<VAR>V W : Set (β × β)<GOAL>UniformSpace.ball x (V ∩ W) = UniformSpace.ball x V ∩ UniformSpace.ball x W
<VAR>β : Type ub<VAR>x : β<VAR>V W : Set (β × β)<GOAL>UniformSpace.ball x (V ∩ W) ⊆ UniformSpace.ball x V
<VAR>β : Type ub<VAR>x : β<VAR>V W : Set (β × β)<GOAL>UniformSpace.ball x (V ∩ W) ⊆ UniformSpace.ball x W
<VAR>β : Type ub<VAR>V : Set (β × β)<VAR>hV : SymmetricRel V<VAR>x y : β<GOAL>x ∈ UniformSpace.ball y V ↔ y ∈ UniformSpace.ball x V
<VAR>β : Type ub<VAR>V : Set (β × β)<VAR>hV : SymmetricRel V<VAR>x : β<GOAL>UniformSpace.ball x V = {y | (y, x) ∈ V}
<VAR>β : Type ub<VAR>V W : Set (β × β)<VAR>x y z : β<VAR>hV : SymmetricRel V<VAR>hx : x ∈ UniformSpace.ball z V<VAR>hy : y ∈ UniformSpace.ball z W<GOAL>(x, y) ∈ V ○ W
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<VAR>V : Set (α × α)<VAR>hV : IsOpen V<GOAL>IsOpen (UniformSpace.ball x V)
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<VAR>V : Set (α × α)<VAR>hV : IsClosed V<GOAL>IsClosed (UniformSpace.ball x V)
<VAR>β : Type ub<VAR>V W M : Set (β × β)<VAR>hW' : SymmetricRel W<VAR>p : β × β<GOAL>p ∈ V ○ M ○ W ↔ (UniformSpace.ball p.1 V ×ˢ UniformSpace.ball p.2 W ∩ M).Nonempty
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<VAR>s : Set α<GOAL>s ∈ 𝓝 x ↔ {p | p.1 = x → p.2 ∈ s} ∈ 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<VAR>s : Set α<GOAL>s ∈ 𝓝 x ↔ {p | p.2 = x → p.1 ∈ s} ∈ 𝓤 α
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<VAR>T : Set α<VAR>hx : x ∈ T<VAR>S : Set α<GOAL>𝓝[S] x = Filter.comap (Prod.mk x) (𝓤 α ⊓ 𝓟 (T ×ˢ S))
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<VAR>S : Set α<GOAL>𝓝[S] x = Filter.comap (Prod.mk x) (𝓤 α ⊓ 𝓟 (Set.univ ×ˢ S))
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set α<GOAL>IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, UniformSpace.ball x V ⊆ s
<VAR>α : Type ua<VAR>ι : Sort u_1<VAR>UniformSpace α<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>h : (𝓤 α).HasBasis p s<VAR>x : α<GOAL>(𝓝 x).HasBasis p fun i => UniformSpace.ball x (s i)
<VAR>α : Type ua<VAR>ι : Sort u_1<VAR>UniformSpace α<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>h : (𝓤 α).HasBasis p s<VAR>x : α<GOAL>(𝓝 x).HasBasis p fun i => {y | (y, x) ∈ s i}
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<GOAL>𝓝 x = Filter.comap (fun y => (y, x)) (𝓤 α)
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<VAR>s : Set α<GOAL>s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, UniformSpace.ball x V ⊆ s
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<VAR>V : Set (α × α)<VAR>V_in : V ∈ 𝓤 α<GOAL>UniformSpace.ball x V ∈ 𝓝 x
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<VAR>S : Set α<VAR>V : Set (α × α)<VAR>x_in : x ∈ S<VAR>V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)<GOAL>UniformSpace.ball x V ∈ 𝓝[S] x
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<VAR>s : Set α<GOAL>s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, SymmetricRel V ∧ UniformSpace.ball x V ⊆ s
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<GOAL>(𝓝 x).HasBasis (fun s => s ∈ 𝓤 α ∧ SymmetricRel s) fun s => UniformSpace.ball x s
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set α<VAR>x : α<GOAL>x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SymmetricRel V → (s ∩ UniformSpace.ball x V).Nonempty
<VAR>α : Type ua<VAR>UniformSpace α<VAR>s : Set α<VAR>x : α<GOAL>x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (UniformSpace.ball x V ∩ s).Nonempty
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x y : α<GOAL>(𝓝 (x, y)).HasBasis (fun s => s ∈ 𝓤 α ∧ SymmetricRel s) fun s => UniformSpace.ball x s ×ˢ UniformSpace.ball y s
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<GOAL>𝓝 x = (𝓤 α).lift' (UniformSpace.ball x)
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<GOAL>𝓝 x = (𝓤 α).lift' fun s => {y | (y, x) ∈ s}
<VAR>α : Type ua<VAR>UniformSpace α<VAR>x : α<VAR>s : Set (α × α)<VAR>h : s ∈ 𝓤 α<GOAL>{y | (x, y) ∈ s} ∈ 𝓝 x
<VAR>α : Type ua<VAR>UniformSpace α<VAR>y : α<VAR>s : Set (α × α)<VAR>h : s ∈ 𝓤 α<GOAL>{x | (x, y) ∈ s} ∈ 𝓝 y
<VAR>α : Type ua<VAR>UniformSpace α<VAR>a : α<VAR>U : Set α<VAR>h : U ∈ 𝓝 a<GOAL>∃ V ∈ 𝓝 a, ∃ t ∈ 𝓤 α, ∀ a' ∈ V, UniformSpace.ball a' t ⊆ U
<VAR>α : Type ua<VAR>UniformSpace α<VAR>a : α<GOAL>Filter.Tendsto (fun a' => (a', a)) (𝓝 a) (𝓤 α)
<VAR>α : Type ua<VAR>UniformSpace α<VAR>a : α<GOAL>Filter.Tendsto (fun a' => (a, a')) (𝓝 a) (𝓤 α)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>x : α<VAR>g : Set α → Filter β<VAR>hg : Monotone g<GOAL>(𝓝 x).lift g = (𝓤 α).lift fun s => g (UniformSpace.ball x s)
<VAR>α : Type ua<VAR>β : Type ub<VAR>UniformSpace α<VAR>x : α<VAR>g : Set α → Filter β<VAR>hg : Monotone g<GOAL>(𝓝 x).lift g = (𝓤 α).lift fun s => g {y | (y, x) ∈ s}
<VAR>α : Type ua<VAR>UniformSpace α<VAR>a b : α<GOAL>𝓝 a ×ˢ 𝓝 b = (𝓤 α).lift fun s => (𝓤 α).lift' fun t => {y | (y, a) ∈ s} ×ˢ {y | (b, y) ∈ t}