Basic results on uniform spaces

Uniform spaces are a generalization of metric spaces and topological groups.

Main definitions

In this file we define a complete lattice structure on the type UniformSpace X of uniform structures on X, as well as the pullback (UniformSpace.comap) of uniform structures coming from the pullback of filters.

Notation

Localized in Uniformity, we have the notation 𝓤 X for the uniformity on a uniform space X, and ○ for composition of relations, seen as terms with type Set (X × X).

References

The formalization uses the books:

• [N. Bourbaki, General Topology][bourbaki1966]
• [I. M. James, Topologies and Uniformities][james1999]

But it makes a more systematic use of the filter library.

Relations, seen as SetRel α α

theorem IsOpen.relComp {α : Type ua} {β : Type ub} {γ : Type uc} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {s : SetRel α β} {t : SetRel β γ} (hs : IsOpen s) (ht : IsOpen t) : IsOpen (s.comp t)

theorem IsOpen.relInv {α : Type ua} {β : Type ub} [TopologicalSpace α] [TopologicalSpace β] {s : SetRel α β} (hs : IsOpen s) : IsOpen s.inv

theorem IsOpen.relImage {α : Type ua} {β : Type ub} [TopologicalSpace α] [TopologicalSpace β] {s : SetRel α β} (hs : IsOpen s) {t : Set α} : IsOpen (s.image t)

theorem IsOpen.relPreimage {α : Type ua} {β : Type ub} [TopologicalSpace α] [TopologicalSpace β] {s : SetRel α β} (hs : IsOpen s) {t : Set β} : IsOpen (s.preimage t)

theorem IsClosed.relInv {α : Type ua} {β : Type ub} [TopologicalSpace α] [TopologicalSpace β] {s : SetRel α β} (hs : IsClosed s) : IsClosed s.inv

theorem IsClosed.relImage_of_finite {α : Type ua} {β : Type ub} [TopologicalSpace α] [TopologicalSpace β] {s : SetRel α β} (hs : IsClosed s) {t : Set α} (ht : t.Finite) : IsClosed (s.image t)

theorem IsClosed.relPreimage_of_finite {α : Type ua} {β : Type ub} [TopologicalSpace α] [TopologicalSpace β] {s : SetRel α β} (hs : IsClosed s) {t : Set β} (ht : t.Finite) : IsClosed (s.preimage t)

theorem eventually_uniformity_iterate_comp_subset {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) (n : ℕ) : ∀ᶠ (t : SetRel α α) in (uniformity α).smallSets, (fun (x : SetRel α α) => t.comp x)^[n] t ⊆ s

If s ∈ 𝓤 α, then for any natural n, for a subset t of a sufficiently small set in 𝓤 α, we have t ○ t ○ ... ○ t ⊆ s (n compositions).

theorem eventually_uniformity_comp_subset {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) : ∀ᶠ (t : SetRel α α) in (uniformity α).smallSets, t.comp t ⊆ s

If s ∈ 𝓤 α, then for a subset t of a sufficiently small set in 𝓤 α, we have t ○ t ⊆ s.

Balls in uniform spaces

theorem UniformSpace.isOpen_ball {α : Type ua} [UniformSpace α] (x : α) {V : SetRel α α} (hV : IsOpen V) : IsOpen (ball x V)

theorem UniformSpace.isClosed_ball {α : Type ua} [UniformSpace α] (x : α) {V : SetRel α α} (hV : IsClosed V) : IsClosed (ball x V)

Neighborhoods in uniform spaces

theorem UniformSpace.hasBasis_nhds_prod {α : Type ua} [UniformSpace α] (x y : α) : (nhds (x, y)).HasBasis (fun (s : Set (α × α)) => s ∈ uniformity α ∧ SetRel.IsSymm s) fun (s : Set (α × α)) => ball x s ×ˢ ball y s

theorem nhds_eq_uniformity_prod {α : Type ua} [UniformSpace α] {a b : α} : nhds (a, b) = (uniformity α).lift' fun (s : SetRel α α) => {y : α | (y, a) ∈ s} ×ˢ {y : α | (b, y) ∈ s}

theorem nhdset_of_mem_uniformity {α : Type ua} [UniformSpace α] {d : SetRel α α} (s : SetRel α α) (hd : d ∈ uniformity α) : ∃ (t : SetRel α α), IsOpen t ∧ s ⊆ t ∧ t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}

theorem nhds_le_uniformity {α : Type ua} [UniformSpace α] (x : α) : nhds (x, x) ≤ uniformity α

Entourages are neighborhoods of the diagonal.

theorem iSup_nhds_le_uniformity {α : Type ua} [UniformSpace α] : ⨆ (x : α), nhds (x, x) ≤ uniformity α

Entourages are neighborhoods of the diagonal.

theorem nhdsSet_diagonal_le_uniformity {α : Type ua} [UniformSpace α] : nhdsSet (Set.diagonal α) ≤ uniformity α

Entourages are neighborhoods of the diagonal.

theorem UniformSpace.has_seq_basis (α : Type ua) [UniformSpace α] [(uniformity α).IsCountablyGenerated] : ∃ (V : ℕ → SetRel α α), (uniformity α).HasAntitoneBasis V ∧ ∀ (n : ℕ), (V n).IsSymm

Closure and interior in uniform spaces

theorem closure_eq_uniformity {α : Type ua} [UniformSpace α] (s : Set (α × α)) : closure s = ⋂ V ∈ {V : Set (α × α) | V ∈ uniformity α ∧ SetRel.IsSymm V}, (SetRel.comp V s).comp V

theorem uniformity_hasBasis_closed {α : Type ua} [UniformSpace α] : (uniformity α).HasBasis (fun (V : SetRel α α) => V ∈ uniformity α ∧ IsClosed V) id

theorem uniformity_eq_uniformity_closure {α : Type ua} [UniformSpace α] : uniformity α = (uniformity α).lift' closure

theorem Filter.HasBasis.uniformity_closure {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ι → Prop} {U : ι → SetRel α α} (h : (uniformity α).HasBasis p U) : (uniformity α).HasBasis p fun (i : ι) => closure (U i)

theorem uniformity_hasBasis_closure {α : Type ua} [UniformSpace α] : (uniformity α).HasBasis (fun (V : SetRel α α) => V ∈ uniformity α) closure

Closed entourages form a basis of the uniformity filter.

theorem closure_eq_inter_uniformity {α : Type ua} [UniformSpace α] {t : SetRel α α} : closure t = ⋂ d ∈ uniformity α, SetRel.comp d (t.comp d)

theorem uniformity_eq_uniformity_interior {α : Type ua} [UniformSpace α] : uniformity α = (uniformity α).lift' interior

theorem interior_mem_uniformity {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) : interior s ∈ uniformity α

theorem mem_uniformity_isClosed {α : Type ua} [UniformSpace α] {s : SetRel α α} (h : s ∈ uniformity α) : ∃ t ∈ uniformity α, IsClosed t ∧ t ⊆ s

theorem isOpen_iff_isOpen_ball_subset {α : Type ua} [UniformSpace α] {s : Set α} : IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ uniformity α, IsOpen V ∧ UniformSpace.ball x V ⊆ s

theorem closure_ball_subset {α : Type ua} [UniformSpace α] {x : α} {V : SetRel α α} : closure (UniformSpace.ball x V) ⊆ UniformSpace.ball x (closure V)

theorem Dense.biUnion_uniformity_ball {α : Type ua} [UniformSpace α] {s : Set α} {U : SetRel α α} (hs : Dense s) (hU : U ∈ uniformity α) : ⋃ x ∈ s, UniformSpace.ball x U = Set.univ

The uniform neighborhoods of all points of a dense set cover the whole space.

theorem DenseRange.iUnion_uniformity_ball {α : Type ua} [UniformSpace α] {ι : Type u_2} {xs : ι → α} (xs_dense : DenseRange xs) {U : SetRel α α} (hU : U ∈ uniformity α) : ⋃ (i : ι), UniformSpace.ball (xs i) U = Set.univ

The uniform neighborhoods of all points of a dense indexed collection cover the whole space.

Uniformity bases

theorem uniformity_hasBasis_open {α : Type ua} [UniformSpace α] : (uniformity α).HasBasis (fun (V : SetRel α α) => V ∈ uniformity α ∧ IsOpen V) id

Open elements of 𝓤 α form a basis of 𝓤 α.

theorem Filter.HasBasis.mem_uniformity_iff {α : Type ua} {β : Type ub} [UniformSpace α] {p : β → Prop} {s : β → SetRel α α} (h : (uniformity α).HasBasis p s) {t : SetRel α α} : t ∈ uniformity α ↔ ∃ (i : β), p i ∧ ∀ (a b : α), (a, b) ∈ s i → (a, b) ∈ t

theorem uniformity_hasBasis_open_symmetric {α : Type ua} [UniformSpace α] : (uniformity α).HasBasis (fun (V : SetRel α α) => V ∈ uniformity α ∧ IsOpen V ∧ V.IsSymm) id

Open elements s : SetRel α α of 𝓤 α such that (x, y) ∈ s ↔ (y, x) ∈ s form a basis of 𝓤 α.

theorem comp_open_symm_mem_uniformity_sets {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) : ∃ t ∈ uniformity α, IsOpen t ∧ SetRel.IsSymm t ∧ SetRel.comp t t ⊆ s

@[instance_reducible]

instance instPartialOrderUniformSpace {α : Type ua} : PartialOrder (UniformSpace α)

Equations

• instPartialOrderUniformSpace = PartialOrder.lift (fun (u : UniformSpace α) => uniformity α) ⋯

theorem UniformSpace.le_def {α : Type ua} {u₁ u₂ : UniformSpace α} : u₁ ≤ u₂ ↔ uniformity α ≤ uniformity α

def UniformSpace.generateFilter {α : Type ua} (f : Filter (α × α)) : UniformSpace α

The finest uniformity coarser than a given filter f : Filter (α × α).

Equations

• One or more equations did not get rendered due to their size.

theorem UniformSpace.mem_uniformity_generateFilter {α : Type ua} {f : Filter (α × α)} {s : SetRel α α} : s ∈ uniformity α ↔ ∃ (seq : ℕ → Set (α × α)), seq 0 = s ∧ ∀ (n : ℕ), seq n ∈ f ⊔ Filter.map Prod.swap f ⊔ Filter.principal SetRel.id ∧ SetRel.comp (seq (n + 1)) (seq (n + 1)) ⊆ seq n

theorem UniformSpace.gc_generateFilter_uniformity {α : Type ua} : GaloisConnection generateFilter (@uniformity α)

def UniformSpace.giGenerateFilter {α : Type ua} : GaloisInsertion generateFilter (@uniformity α)

Galois insertion between generateFilter and uniformity.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance instInfSetUniformSpace {α : Type ua} : InfSet (UniformSpace α)

Equations

• instInfSetUniformSpace = { sInf := fun (s : Set (UniformSpace α)) => UniformSpace.ofCore { uniformity := ⨅ u ∈ s, uniformity α, refl := ⋯, symm := ⋯, comp := ⋯ } }

theorem UniformSpace.sInf_le {α : Type ua} {tt : Set (UniformSpace α)} {t : UniformSpace α} (h : t ∈ tt) : sInf tt ≤ t

theorem UniformSpace.le_sInf {α : Type ua} {tt : Set (UniformSpace α)} {t : UniformSpace α} (h : ∀ t' ∈ tt, t ≤ t') : t ≤ sInf tt

theorem UniformSpace.isGLB_sInf {α : Type ua} {tt : Set (UniformSpace α)} : IsGLB tt (sInf tt)

@[instance_reducible]

instance instTopUniformSpace {α : Type ua} : Top (UniformSpace α)

Equations

• instTopUniformSpace = { top := { toTopologicalSpace := ⊤, uniformity := ⊤, symm := ⋯, comp := ⋯, nhds_eq_comap_uniformity := ⋯ } }

@[instance_reducible]

instance instBotUniformSpace {α : Type ua} : Bot (UniformSpace α)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance instMinUniformSpace {α : Type ua} : Min (UniformSpace α)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance instCompleteLatticeUniformSpace {α : Type ua} : CompleteLattice (UniformSpace α)

Equations

• One or more equations did not get rendered due to their size.

theorem iInf_uniformity {α : Type ua} {ι : Sort u_2} {u : ι → UniformSpace α} : uniformity α = ⨅ (i : ι), uniformity α

theorem inf_uniformity {α : Type ua} {u v : UniformSpace α} : uniformity α = uniformity α ⊓ uniformity α

theorem bot_uniformity {α : Type ua} : uniformity α = Filter.principal SetRel.id

theorem top_uniformity {α : Type ua} : uniformity α = ⊤

@[instance_reducible]

instance inhabitedUniformSpace {α : Type ua} : Inhabited (UniformSpace α)

Equations

• inhabitedUniformSpace = { default := ⊥ }

@[instance_reducible]

instance inhabitedUniformSpaceCore {α : Type ua} : Inhabited (UniformSpace.Core α)

Equations

• inhabitedUniformSpaceCore = { default := default.toCore }

@[instance_reducible]

instance instUniqueUniformSpaceOfSubsingleton {α : Type ua} [Subsingleton α] : Unique (UniformSpace α)

Equations

• instUniqueUniformSpaceOfSubsingleton = { toInhabited := inhabitedUniformSpace, uniq := ⋯ }

@[reducible, inline]

abbrev UniformSpace.comap {α : Type ua} {β : Type ub} (f : α → β) (u : UniformSpace β) : UniformSpace α

Given f : α → β and a uniformity u on β, the inverse image of u under f is the inverse image in the filter sense of the induced function α × α → β × β. See note [reducible non-instances].

Equations

• One or more equations did not get rendered due to their size.

theorem uniformity_comap {α : Type ua} {β : Type ub} {x✝ : UniformSpace β} (f : α → β) : uniformity α = Filter.comap (Prod.map f f) (uniformity β)

theorem ball_preimage {α : Type ua} {β : Type ub} {f : α → β} {U : SetRel β β} {x : α} : UniformSpace.ball x (Prod.map f f ⁻¹' U) = f ⁻¹' UniformSpace.ball (f x) U

@[simp]

theorem UniformSpace.comap_id {α : Type u_2} : comap id = id

@[deprecated UniformSpace.comap_id (since := "2026-10-13")]

theorem uniformSpace_comap_id {α : Type u_2} : UniformSpace.comap id = id

Alias of UniformSpace.comap_id.

theorem UniformSpace.comap_comap {α : Type u_2} {β : Type u_3} {γ : Type u_4} {uγ : UniformSpace γ} {f : α → β} {g : β → γ} : comap (g ∘ f) uγ = comap f (comap g uγ)

theorem UniformSpace.comap_inf {α : Type u_2} {γ : Type u_3} {u₁ u₂ : UniformSpace γ} {f : α → γ} : comap f (u₁ ⊓ u₂) = comap f u₁ ⊓ comap f u₂

theorem UniformSpace.comap_iInf {ι : Sort u_2} {α : Type u_3} {γ : Type u_4} {u : ι → UniformSpace γ} {f : α → γ} : comap f (⨅ (i : ι), u i) = ⨅ (i : ι), comap f (u i)

theorem UniformSpace.comap_monotone {α : Type u_2} {γ : Type u_3} {f : α → γ} : Monotone fun (u : UniformSpace γ) => comap f u

@[deprecated UniformSpace.comap_monotone (since := "2026-10-13")]

theorem UniformSpace.comap_mono {α : Type u_2} {γ : Type u_3} {f : α → γ} : Monotone fun (u : UniformSpace γ) => comap f u

Alias of UniformSpace.comap_monotone.

theorem uniformContinuous_iff_le_comap {α : Type u_2} {β : Type u_3} {uα : UniformSpace α} {uβ : UniformSpace β} {f : α → β} : UniformContinuous f ↔ uα ≤ UniformSpace.comap f uβ

@[deprecated uniformContinuous_iff_le_comap (since := "2026-05-23")]

theorem uniformContinuous_iff {α : Type u_2} {β : Type u_3} {uα : UniformSpace α} {uβ : UniformSpace β} {f : α → β} : UniformContinuous f ↔ uα ≤ UniformSpace.comap f uβ

Alias of uniformContinuous_iff_le_comap.

theorem le_iff_uniformContinuous_id {α : Type ua} {u v : UniformSpace α} : u ≤ v ↔ UniformContinuous id

theorem uniformContinuous_comap {α : Type ua} {β : Type ub} {f : α → β} [u : UniformSpace β] : UniformContinuous f

theorem uniformContinuous_comap' {α : Type ua} {β : Type ub} {γ : Type uc} {f : γ → β} {g : α → γ} [v : UniformSpace β] [u : UniformSpace α] (h : UniformContinuous (f ∘ g)) : UniformContinuous g

def UniformSpace.map {α : Type ua} {β : Type ub} (f : α → β) (u : UniformSpace α) : UniformSpace β

Given f : α → β and a uniformity u on α, the image of u under f is the finest uniformity on β making the map f uniformly continuous. You almost never want to put this as an instance on a type, and it does not always agree with the coinduced topology.

Equations

• UniformSpace.map f u = UniformSpace.generateFilter (Filter.map (Prod.map f f) (uniformity α))

theorem UniformSpace.gc_map_comap {α : Type ua} {β : Type ub} (f : α → β) : GaloisConnection (map f) (comap f)

@[simp]

theorem UniformSpace.map_id {α : Type u_2} : map id = id

theorem UniformSpace.map_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} {uα : UniformSpace α} {f : α → β} {g : β → γ} : map (g ∘ f) uα = map g (map f uα)

theorem UniformSpace.map_sup {α : Type u_2} {γ : Type u_3} {u₁ u₂ : UniformSpace α} {f : α → γ} : map f (u₁ ⊔ u₂) = map f u₁ ⊔ map f u₂

theorem UniformSpace.map_iSup {ι : Sort u_2} {α : Type u_3} {γ : Type u_4} {u : ι → UniformSpace α} {f : α → γ} : map f (⨆ (i : ι), u i) = ⨆ (i : ι), map f (u i)

theorem UniformSpace.map_monotone {α : Type u_2} {γ : Type u_3} {f : α → γ} : Monotone fun (u : UniformSpace α) => map f u

theorem uniformContinuous_iff_map_le {α : Type u_2} {β : Type u_3} {uα : UniformSpace α} {uβ : UniformSpace β} {f : α → β} : UniformContinuous f ↔ UniformSpace.map f uα ≤ uβ

theorem uniformContinuous_map {α : Type ua} {β : Type ub} {f : α → β} [u : UniformSpace α] : UniformContinuous f

theorem uniformContinuous_map' {α : Type ua} {β : Type ub} {γ : Type uc} {f : α → γ} {g : γ → β} [u : UniformSpace α] [v : UniformSpace β] (h : UniformContinuous (g ∘ f)) : UniformContinuous g

theorem UniformSpace.to_nhds_mono {α : Type ua} {u₁ u₂ : UniformSpace α} (h : u₁ ≤ u₂) (a : α) : nhds a ≤ nhds a

theorem UniformSpace.toTopologicalSpace_mono {α : Type ua} {u₁ u₂ : UniformSpace α} (h : u₁ ≤ u₂) : u₁.toTopologicalSpace ≤ u₂.toTopologicalSpace

theorem UniformSpace.toTopologicalSpace_comap {α : Type ua} {β : Type ub} {f : α → β} {u : UniformSpace β} : (comap f u).toTopologicalSpace = TopologicalSpace.induced f u.toTopologicalSpace

theorem UniformSpace.uniformSpace_eq_bot {α : Type ua} {u : UniformSpace α} : u = ⊥ ↔ SetRel.id ∈ uniformity α

theorem Filter.HasBasis.uniformSpace_eq_bot {α : Type ua} {ι : Sort u_2} {p : ι → Prop} {s : ι → SetRel α α} {u : UniformSpace α} (h : (uniformity α).HasBasis p s) : u = ⊥ ↔ ∃ (i : ι), p i ∧ Pairwise fun (x y : α) => (x, y) ∉ s i

theorem UniformSpace.toTopologicalSpace_bot {α : Type ua} : ⊥.toTopologicalSpace = ⊥

theorem UniformSpace.toTopologicalSpace_top {α : Type ua} : ⊤.toTopologicalSpace = ⊤

theorem UniformSpace.toTopologicalSpace_iInf {α : Type ua} {ι : Sort u_2} {u : ι → UniformSpace α} : (iInf u).toTopologicalSpace = ⨅ (i : ι), (u i).toTopologicalSpace

theorem UniformSpace.toTopologicalSpace_sInf {α : Type ua} {s : Set (UniformSpace α)} : (sInf s).toTopologicalSpace = ⨅ i ∈ s, i.toTopologicalSpace

theorem UniformSpace.toTopologicalSpace_inf {α : Type ua} {u v : UniformSpace α} : (u ⊓ v).toTopologicalSpace = u.toTopologicalSpace ⊓ v.toTopologicalSpace

theorem UniformContinuous.continuous {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} (hf : UniformContinuous f) : Continuous f

theorem UniformContinuous.uniformContinuousOn {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} (hf : UniformContinuous f) : UniformContinuousOn f s

theorem UniformContinuousOn.mono {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} {s t : Set α} (hf : UniformContinuousOn f s) (ht : t ⊆ s) : UniformContinuousOn f t

theorem UniformContinuousOn.congr {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f g : α → β} {s : Set α} (hf : UniformContinuousOn f s) (h : Set.EqOn f g s) : UniformContinuousOn g s

theorem UniformContinuousOn.comp {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : α → β} {s : Set α} {g : β → γ} {t : Set β} (hg : UniformContinuousOn g t) (hf : UniformContinuousOn f s) (hst : Set.MapsTo f s t) : UniformContinuousOn (g ∘ f) s

theorem UniformContinuous.comp_uniformContinuousOn {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : α → β} {s : Set α} {g : β → γ} (hg : UniformContinuous g) (hf : UniformContinuousOn f s) : UniformContinuousOn (g ∘ f) s

@[instance_reducible]

instance ULift.uniformSpace {α : Type ua} [UniformSpace α] : UniformSpace (ULift.{u_2, ua} α)

Uniform space structure on ULift α.

Equations

• ULift.uniformSpace = UniformSpace.comap ULift.down inst✝

@[instance_reducible]

instance OrderDual.instUniformSpace {α : Type ua} [UniformSpace α] : UniformSpace αᵒᵈ

Uniform space structure on αᵒᵈ.

Equations

• OrderDual.instUniformSpace = inst✝

theorem UniformContinuous.inf_rng {α : Type ua} {β : Type ub} {f : α → β} {u₁ : UniformSpace α} {u₂ u₃ : UniformSpace β} (h₁ : UniformContinuous f) (h₂ : UniformContinuous f) : UniformContinuous f

theorem UniformContinuous.inf_dom_left {α : Type ua} {β : Type ub} {f : α → β} {u₁ u₂ : UniformSpace α} {u₃ : UniformSpace β} (hf : UniformContinuous f) : UniformContinuous f

theorem UniformContinuous.inf_dom_right {α : Type ua} {β : Type ub} {f : α → β} {u₁ u₂ : UniformSpace α} {u₃ : UniformSpace β} (hf : UniformContinuous f) : UniformContinuous f

theorem uniformContinuous_sInf_dom {α : Type ua} {β : Type ub} {f : α → β} {u₁ : Set (UniformSpace α)} {u₂ : UniformSpace β} {u : UniformSpace α} (h₁ : u ∈ u₁) (hf : UniformContinuous f) : UniformContinuous f

theorem uniformContinuous_sInf_rng {α : Type ua} {β : Type ub} {f : α → β} {u₁ : UniformSpace α} {u₂ : Set (UniformSpace β)} : UniformContinuous f ↔ ∀ u ∈ u₂, UniformContinuous f

theorem uniformContinuous_iInf_dom {α : Type ua} {β : Type ub} {ι : Sort u_1} {f : α → β} {u₁ : ι → UniformSpace α} {u₂ : UniformSpace β} {i : ι} (hf : UniformContinuous f) : UniformContinuous f

theorem uniformContinuous_iInf_rng {α : Type ua} {β : Type ub} {ι : Sort u_1} {f : α → β} {u₁ : UniformSpace α} {u₂ : ι → UniformSpace β} : UniformContinuous f ↔ ∀ (i : ι), UniformContinuous f

theorem discreteTopology_of_discrete_uniformity {α : Type ua} [hα : UniformSpace α] (h : uniformity α = Filter.principal SetRel.id) : DiscreteTopology α

A uniform space with the discrete uniformity has the discrete topology.

@[instance_reducible]

instance instUniformSpaceEmpty : UniformSpace Empty

Equations

• instUniformSpaceEmpty = ⊥

@[instance_reducible]

instance instUniformSpacePUnit : UniformSpace PUnit.{u_2 + 1}

Equations

• instUniformSpacePUnit = ⊥

@[instance_reducible]

instance instUniformSpaceBool : UniformSpace Bool

Equations

• instUniformSpaceBool = ⊥

@[instance_reducible]

instance instUniformSpaceNat : UniformSpace ℕ

Equations

• instUniformSpaceNat = ⊥

@[instance_reducible]

instance instUniformSpaceInt : UniformSpace ℤ

Equations

• instUniformSpaceInt = ⊥

@[instance_reducible]

instance instUniformSpaceAdditive {α : Type ua} [UniformSpace α] : UniformSpace (Additive α)

Equations

• instUniformSpaceAdditive = inst✝

@[instance_reducible]

instance instUniformSpaceMultiplicative {α : Type ua} [UniformSpace α] : UniformSpace (Multiplicative α)

Equations

• instUniformSpaceMultiplicative = inst✝

theorem uniformContinuous_ofMul {α : Type ua} [UniformSpace α] : UniformContinuous ⇑Additive.ofMul

theorem uniformContinuous_toMul {α : Type ua} [UniformSpace α] : UniformContinuous ⇑Additive.toMul

theorem uniformContinuous_ofAdd {α : Type ua} [UniformSpace α] : UniformContinuous ⇑Multiplicative.ofAdd

theorem uniformContinuous_toAdd {α : Type ua} [UniformSpace α] : UniformContinuous ⇑Multiplicative.toAdd

theorem uniformity_additive {α : Type ua} [UniformSpace α] : uniformity (Additive α) = Filter.map (Prod.map ⇑Additive.ofMul ⇑Additive.ofMul) (uniformity α)

theorem uniformity_multiplicative {α : Type ua} [UniformSpace α] : uniformity (Multiplicative α) = Filter.map (Prod.map ⇑Multiplicative.ofAdd ⇑Multiplicative.ofAdd) (uniformity α)

@[instance_reducible]

instance instUniformSpaceSubtype {α : Type ua} {p : α → Prop} [t : UniformSpace α] : UniformSpace (Subtype p)

Equations

• instUniformSpaceSubtype = UniformSpace.comap Subtype.val t

theorem uniformity_subtype {α : Type ua} {p : α → Prop} [UniformSpace α] : uniformity (Subtype p) = Filter.comap (fun (q : Subtype p × Subtype p) => (↑q.1, ↑q.2)) (uniformity α)

theorem uniformity_setCoe {α : Type ua} {s : Set α} [UniformSpace α] : uniformity ↑s = Filter.comap (Prod.map Subtype.val Subtype.val) (uniformity α)

theorem map_uniformity_set_coe {α : Type ua} {s : Set α} [UniformSpace α] : Filter.map (Prod.map Subtype.val Subtype.val) (uniformity ↑s) = uniformity α ⊓ Filter.principal (s ×ˢ s)

theorem uniformContinuous_subtype_val {α : Type ua} {p : α → Prop} [UniformSpace α] : UniformContinuous Subtype.val

theorem UniformContinuous.subtype_mk {α : Type ua} {β : Type ub} {p : α → Prop} [UniformSpace α] [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (h : ∀ (x : β), p (f x)) : UniformContinuous fun (x : β) => ⟨f x, ⋯⟩

theorem UniformContinuous.subtype_map {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {p : α → Prop} {q : β → Prop} {f : α → β} (hf : UniformContinuous f) (h : ∀ (x : α), p x → q (f x)) : UniformContinuous (Subtype.map f h)

theorem uniformContinuousOn_iff_restrict {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} : UniformContinuousOn f s ↔ UniformContinuous (s.domRestrict f)

theorem UniformContinuousOn.restrict {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} : UniformContinuousOn f s → UniformContinuous (s.domRestrict f)

Alias of the forward direction of uniformContinuousOn_iff_restrict.

theorem UniformContinuousOn.of_restrict {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} : UniformContinuous (s.domRestrict f) → UniformContinuousOn f s

Alias of the reverse direction of uniformContinuousOn_iff_restrict.

theorem tendsto_of_uniformContinuous_subtype {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} {a : α} (hf : UniformContinuous fun (x : ↑s) => f ↑x) (ha : s ∈ nhds a) : Filter.Tendsto f (nhds a) (nhds (f a))

theorem UniformContinuousOn.continuousOn {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} (h : UniformContinuousOn f s) : ContinuousOn f s

instance instIsCountablyGeneratedProdElemUniformity {α : Type ua} [UniformSpace α] [(uniformity α).IsCountablyGenerated] (s : Set α) : (uniformity ↑s).IsCountablyGenerated

@[instance_reducible]

instance instUniformSpaceMulOpposite {α : Type ua} [UniformSpace α] : UniformSpace αᵐᵒᵖ

Equations

• instUniformSpaceMulOpposite = UniformSpace.comap MulOpposite.unop inst✝

@[instance_reducible]

instance instUniformSpaceAddOpposite {α : Type ua} [UniformSpace α] : UniformSpace αᵃᵒᵖ

Equations

• instUniformSpaceAddOpposite = UniformSpace.comap AddOpposite.unop inst✝

theorem uniformity_mulOpposite {α : Type ua} [UniformSpace α] : uniformity αᵐᵒᵖ = Filter.comap (fun (q : αᵐᵒᵖ × αᵐᵒᵖ) => (MulOpposite.unop q.1, MulOpposite.unop q.2)) (uniformity α)

theorem uniformity_addOpposite {α : Type ua} [UniformSpace α] : uniformity αᵃᵒᵖ = Filter.comap (fun (q : αᵃᵒᵖ × αᵃᵒᵖ) => (AddOpposite.unop q.1, AddOpposite.unop q.2)) (uniformity α)

@[simp]

theorem comap_uniformity_mulOpposite {α : Type ua} [UniformSpace α] : Filter.comap (fun (p : α × α) => (MulOpposite.op p.1, MulOpposite.op p.2)) (uniformity αᵐᵒᵖ) = uniformity α

@[simp]

theorem comap_uniformity_addOpposite {α : Type ua} [UniformSpace α] : Filter.comap (fun (p : α × α) => (AddOpposite.op p.1, AddOpposite.op p.2)) (uniformity αᵃᵒᵖ) = uniformity α

theorem MulOpposite.uniformContinuous_unop {α : Type ua} [UniformSpace α] : UniformContinuous unop

theorem AddOpposite.uniformContinuous_unop {α : Type ua} [UniformSpace α] : UniformContinuous unop

theorem MulOpposite.uniformContinuous_op {α : Type ua} [UniformSpace α] : UniformContinuous op

theorem AddOpposite.uniformContinuous_op {α : Type ua} [UniformSpace α] : UniformContinuous op

theorem MulOpposite.isUniformEmbedding_unop {α : Type ua} [UniformSpace α] : IsUniformEmbedding unop

theorem AddOpposite.isUniformEmbedding_unop {α : Type ua} [UniformSpace α] : IsUniformEmbedding unop

theorem MulOpposite.isUniformEmbedding_op {α : Type ua} [UniformSpace α] : IsUniformEmbedding op

theorem AddOpposite.isUniformEmbedding_op {α : Type ua} [UniformSpace α] : IsUniformEmbedding op

a similar product space is possible on the function space (uniformity of pointwise convergence), but we want to have the uniformity of uniform convergence on function spaces

@[instance_reducible]

instance instUniformSpaceProd {α : Type ua} {β : Type ub} [u₁ : UniformSpace α] [u₂ : UniformSpace β] : UniformSpace (α × β)

Equations

• instUniformSpaceProd = UniformSpace.comap Prod.fst u₁ ⊓ UniformSpace.comap Prod.snd u₂

theorem uniformity_prod {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : uniformity (α × β) = Filter.comap (fun (p : (α × β) × α × β) => (p.1.1, p.2.1)) (uniformity α) ⊓ Filter.comap (fun (p : (α × β) × α × β) => (p.1.2, p.2.2)) (uniformity β)

instance instIsCountablyGeneratedProdUniformity {α : Type ua} {β : Type ub} [UniformSpace α] [(uniformity α).IsCountablyGenerated] [UniformSpace β] [(uniformity β).IsCountablyGenerated] : (uniformity (α × β)).IsCountablyGenerated

theorem uniformity_prod_eq_comap_prod {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : uniformity (α × β) = Filter.comap (fun (p : (α × β) × α × β) => ((p.1.1, p.2.1), p.1.2, p.2.2)) (uniformity α ×ˢ uniformity β)

theorem uniformity_prod_eq_prod {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : uniformity (α × β) = Filter.map (fun (p : (α × α) × β × β) => ((p.1.1, p.2.1), p.1.2, p.2.2)) (uniformity α ×ˢ uniformity β)

theorem mem_uniformity_of_uniformContinuous_invariant {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {s : SetRel β β} {f : α → α → β} (hf : UniformContinuous fun (p : α × α) => f p.1 p.2) (hs : s ∈ uniformity β) : ∃ u ∈ uniformity α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s

def entourageProd {α : Type ua} {β : Type ub} (u : SetRel α α) (v : SetRel β β) : SetRel (α × β) (α × β)

An entourage of the diagonal in α and an entourage in β yield an entourage in α × β once we permute coordinates.

Equations

• entourageProd u v = {((a₁, b₁), a₂, b₂) : (α × β) × α × β | (a₁, a₂) ∈ u ∧ (b₁, b₂) ∈ v}

theorem mem_entourageProd {α : Type ua} {β : Type ub} {u : SetRel α α} {v : SetRel β β} {p : (α × β) × α × β} : p ∈ entourageProd u v ↔ (p.1.1, p.2.1) ∈ u ∧ (p.1.2, p.2.2) ∈ v

theorem entourageProd_mem_uniformity {α : Type ua} {β : Type ub} [t₁ : UniformSpace α] [t₂ : UniformSpace β] {u : SetRel α α} {v : SetRel β β} (hu : u ∈ uniformity α) (hv : v ∈ uniformity β) : entourageProd u v ∈ uniformity (α × β)

theorem ball_entourageProd {α : Type ua} {β : Type ub} (u : SetRel α α) (v : SetRel β β) (x : α × β) : UniformSpace.ball x (entourageProd u v) = UniformSpace.ball x.1 u ×ˢ UniformSpace.ball x.2 v

instance IsSymm_entourageProd {α : Type ua} {β : Type ub} {u : SetRel α α} {v : SetRel β β} [u.IsSymm] [v.IsSymm] : (entourageProd u v).IsSymm

@[simp]

theorem inv_entourageProd {α : Type ua} {β : Type ub} (u : SetRel α α) (v : SetRel β β) : (entourageProd u v).inv = entourageProd u.inv v.inv

@[simp]

theorem image_entourageProd_prod {α : Type ua} {β : Type ub} (u : SetRel α α) (v : SetRel β β) (s : Set α) (t : Set β) : (entourageProd u v).image (s ×ˢ t) = u.image s ×ˢ v.image t

@[simp]

theorem preimage_entourageProd_prod {α : Type ua} {β : Type ub} (u : SetRel α α) (v : SetRel β β) (s : Set α) (t : Set β) : (entourageProd u v).preimage (s ×ˢ t) = u.preimage s ×ˢ v.preimage t

theorem Filter.HasBasis.uniformity_prod {α : Type ua} {β : Type ub} {ιa : Type u_2} {ιb : Type u_3} [UniformSpace α] [UniformSpace β] {pa : ιa → Prop} {pb : ιb → Prop} {sa : ιa → SetRel α α} {sb : ιb → SetRel β β} (ha : (uniformity α).HasBasis pa sa) (hb : (uniformity β).HasBasis pb sb) : (uniformity (α × β)).HasBasis (fun (i : ιa × ιb) => pa i.1 ∧ pb i.2) fun (i : ιa × ιb) => entourageProd (sa i.1) (sb i.2)

theorem entourageProd_subset {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {s : Set ((α × β) × α × β)} (h : s ∈ uniformity (α × β)) : ∃ u ∈ uniformity α, ∃ v ∈ uniformity β, entourageProd u v ⊆ s

theorem tendsto_prod_uniformity_fst {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : Filter.Tendsto (fun (p : (α × β) × α × β) => (p.1.1, p.2.1)) (uniformity (α × β)) (uniformity α)

theorem tendsto_prod_uniformity_snd {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : Filter.Tendsto (fun (p : (α × β) × α × β) => (p.1.2, p.2.2)) (uniformity (α × β)) (uniformity β)

theorem uniformContinuous_fst {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : UniformContinuous fun (p : α × β) => p.1

theorem uniformContinuous_snd {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : UniformContinuous fun (p : α × β) => p.2

theorem UniformContinuous.prodMk {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f₁ : α → β} {f₂ : α → γ} (h₁ : UniformContinuous f₁) (h₂ : UniformContinuous f₂) : UniformContinuous fun (a : α) => (f₁ a, f₂ a)

theorem UniformContinuous.prodMk_left {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : α × β → γ} (h : UniformContinuous f) (b : β) : UniformContinuous fun (a : α) => f (a, b)

theorem UniformContinuous.prodMk_right {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : α × β → γ} (h : UniformContinuous f) (a : α) : UniformContinuous fun (b : β) => f (a, b)

theorem UniformContinuous.prodMap {α : Type ua} {β : Type ub} {γ : Type uc} {δ : Type ud} [UniformSpace α] [UniformSpace β] [UniformSpace γ] [UniformSpace δ] {f : α → γ} {g : β → δ} (hf : UniformContinuous f) (hg : UniformContinuous g) : UniformContinuous (Prod.map f g)

theorem uniformContinuous_swap {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : UniformContinuous Prod.swap

theorem toTopologicalSpace_prod {α : Type u_2} {β : Type u_3} [u : UniformSpace α] [v : UniformSpace β] : instUniformSpaceProd.toTopologicalSpace = instTopologicalSpaceProd

theorem uniformContinuous_inf_dom_left₂ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : α → β → γ} {ua1 ua2 : UniformSpace α} {ub1 ub2 : UniformSpace β} {uc1 : UniformSpace γ} (h : UniformContinuous fun (p : α × β) => f p.1 p.2) : UniformContinuous fun (p : α × β) => f p.1 p.2

A version of UniformContinuous.inf_dom_left for binary functions

theorem uniformContinuous_inf_dom_right₂ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : α → β → γ} {ua1 ua2 : UniformSpace α} {ub1 ub2 : UniformSpace β} {uc1 : UniformSpace γ} (h : UniformContinuous fun (p : α × β) => f p.1 p.2) : UniformContinuous fun (p : α × β) => f p.1 p.2

A version of UniformContinuous.inf_dom_right for binary functions

theorem uniformContinuous_sInf_dom₂ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : α → β → γ} {uas : Set (UniformSpace α)} {ubs : Set (UniformSpace β)} {ua : UniformSpace α} {ub : UniformSpace β} {uc : UniformSpace γ} (ha : ua ∈ uas) (hb : ub ∈ ubs) (hf : UniformContinuous fun (p : α × β) => f p.1 p.2) : UniformContinuous fun (p : α × β) => f p.1 p.2

A version of uniformContinuous_sInf_dom for binary functions

def UniformContinuous₂ {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] (f : α → β → γ) : Prop

Uniform continuity for functions of two variables.

Equations

• UniformContinuous₂ f = UniformContinuous (Function.uncurry f)

theorem uniformContinuous₂_def {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] (f : α → β → γ) : UniformContinuous₂ f ↔ UniformContinuous (Function.uncurry f)

theorem UniformContinuous₂.uniformContinuous {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : α → β → γ} (h : UniformContinuous₂ f) : UniformContinuous (Function.uncurry f)

theorem uniformContinuous₂_curry {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] (f : α × β → γ) : UniformContinuous₂ (Function.curry f) ↔ UniformContinuous f

theorem UniformContinuous₂.comp {α : Type ua} {β : Type ub} {γ : Type uc} {δ : Type ud} [UniformSpace α] [UniformSpace β] [UniformSpace γ] [UniformSpace δ] {f : α → β → γ} {g : γ → δ} (hg : UniformContinuous g) (hf : UniformContinuous₂ f) : UniformContinuous₂ (Function.bicompr g f)

theorem UniformContinuous₂.bicompl {α : Type ua} {β : Type ub} {γ : Type uc} {δ : Type ud} {δ' : Type u_2} [UniformSpace α] [UniformSpace β] [UniformSpace γ] [UniformSpace δ] [UniformSpace δ'] {f : α → β → γ} {ga : δ → α} {gb : δ' → β} (hf : UniformContinuous₂ f) (hga : UniformContinuous ga) (hgb : UniformContinuous gb) : UniformContinuous₂ (Function.bicompl f ga gb)

theorem toTopologicalSpace_subtype {α : Type ua} [u : UniformSpace α] {p : α → Prop} : instUniformSpaceSubtype.toTopologicalSpace = instTopologicalSpaceSubtype

@[instance_reducible]

instance Sum.instUniformSpace {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : UniformSpace (α ⊕ β)

Uniformity on a disjoint union. Entourages of the diagonal in the union are obtained by taking independently an entourage of the diagonal in the first part, and an entourage of the diagonal in the second part.

Equations

• One or more equations did not get rendered due to their size.

theorem union_mem_uniformity_sum {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {a : SetRel α α} (ha : a ∈ uniformity α) {b : SetRel β β} (hb : b ∈ uniformity β) : Prod.map Sum.inl Sum.inl '' a ∪ Prod.map Sum.inr Sum.inr '' b ∈ uniformity (α ⊕ β)

The union of an entourage of the diagonal in each set of a disjoint union is again an entourage of the diagonal.

theorem Sum.uniformity {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : _root_.uniformity (α ⊕ β) = Filter.map (Prod.map inl inl) (_root_.uniformity α) ⊔ Filter.map (Prod.map inr inr) (_root_.uniformity β)

theorem uniformContinuous_inl {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : UniformContinuous Sum.inl

theorem uniformContinuous_inr {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : UniformContinuous Sum.inr

instance instIsCountablyGeneratedProdSumUniformity {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] [(uniformity α).IsCountablyGenerated] [(uniformity β).IsCountablyGenerated] : (uniformity (α ⊕ β)).IsCountablyGenerated

Expressing continuity properties in uniform spaces

We reformulate the various continuity properties of functions taking values in a uniform space in terms of the uniformity in the target. Since the same lemmas (essentially with the same names) also exist for metric spaces and emetric spaces (reformulating things in terms of the distance or the edistance in the target), we put them in a namespace Uniform here.

In the metric and emetric space setting, there are also similar lemmas where one assumes that both the source and the target are metric spaces, reformulating things in terms of the distance on both sides. These lemmas are generally written without primes, and the versions where only the target is a metric space is primed. We follow the same convention here, thus giving lemmas with primes.

theorem Uniform.tendsto_nhds_right {α : Type ua} {β : Type ub} [UniformSpace α] {f : Filter β} {u : β → α} {a : α} : Filter.Tendsto u f (nhds a) ↔ Filter.Tendsto (fun (x : β) => (a, u x)) f (uniformity α)

theorem Uniform.tendsto_nhds_left {α : Type ua} {β : Type ub} [UniformSpace α] {f : Filter β} {u : β → α} {a : α} : Filter.Tendsto u f (nhds a) ↔ Filter.Tendsto (fun (x : β) => (u x, a)) f (uniformity α)

theorem Uniform.continuousAt_iff'_right {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} {b : β} : ContinuousAt f b ↔ Filter.Tendsto (fun (x : β) => (f b, f x)) (nhds b) (uniformity α)

theorem Uniform.continuousAt_iff'_left {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} {b : β} : ContinuousAt f b ↔ Filter.Tendsto (fun (x : β) => (f x, f b)) (nhds b) (uniformity α)

theorem Uniform.continuousAt_iff_prod {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} {b : β} : ContinuousAt f b ↔ Filter.Tendsto (fun (x : β × β) => (f x.1, f x.2)) (nhds (b, b)) (uniformity α)

theorem Uniform.continuousWithinAt_iff'_right {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} : ContinuousWithinAt f s b ↔ Filter.Tendsto (fun (x : β) => (f b, f x)) (nhdsWithin b s) (uniformity α)

theorem Uniform.continuousWithinAt_iff'_left {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} : ContinuousWithinAt f s b ↔ Filter.Tendsto (fun (x : β) => (f x, f b)) (nhdsWithin b s) (uniformity α)

theorem Uniform.continuousOn_iff'_right {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} {s : Set β} : ContinuousOn f s ↔ ∀ b ∈ s, Filter.Tendsto (fun (x : β) => (f b, f x)) (nhdsWithin b s) (uniformity α)

theorem Uniform.continuousOn_iff'_left {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} {s : Set β} : ContinuousOn f s ↔ ∀ b ∈ s, Filter.Tendsto (fun (x : β) => (f x, f b)) (nhdsWithin b s) (uniformity α)

theorem Uniform.continuous_iff'_right {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} : Continuous f ↔ ∀ (b : β), Filter.Tendsto (fun (x : β) => (f b, f x)) (nhds b) (uniformity α)

theorem Uniform.continuous_iff'_left {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {f : β → α} : Continuous f ↔ ∀ (b : β), Filter.Tendsto (fun (x : β) => (f x, f b)) (nhds b) (uniformity α)

theorem Uniform.exists_is_open_mem_uniformity_of_forall_mem_eq {α : Type ua} {β : Type ub} [UniformSpace α] [TopologicalSpace β] {r : SetRel α α} {s : Set β} {f g : β → α} (hf : ∀ x ∈ s, ContinuousAt f x) (hg : ∀ x ∈ s, ContinuousAt g x) (hfg : Set.EqOn f g s) (hr : r ∈ uniformity α) : ∃ (t : Set β), IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, (f x, g x) ∈ r

Consider two functions f and g which coincide on a set s and are continuous there. Then there is an open neighborhood of s on which f and g are uniformly close.

theorem Filter.Tendsto.congr_uniformity {α : Type u_2} {β : Type u_3} [UniformSpace β] {f g : α → β} {l : Filter α} {b : β} (hf : Tendsto f l (nhds b)) (hg : Tendsto (fun (x : α) => (f x, g x)) l (uniformity β)) : Tendsto g l (nhds b)

theorem Uniform.tendsto_congr {α : Type u_2} {β : Type u_3} [UniformSpace β] {f g : α → β} {l : Filter α} {b : β} (hfg : Filter.Tendsto (fun (x : α) => (f x, g x)) l (uniformity β)) : Filter.Tendsto f l (nhds b) ↔ Filter.Tendsto g l (nhds b)