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. Like distance functions, uniform structures cannot be pushed forward in general.

Notations

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
• [I. M. James, Topologies and Uniformities][james1999]

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

Relations, seen as Set (α × α)

theorem eventually_uniformity_iterate_comp_subset {α : Type ua} [UniformSpace α] {s : Set (α × α)} (hs : s ∈ uniformity α) (n : ℕ) : ∀ᶠ (t : Set (α × α)) in (uniformity α).smallSets, (fun (x : Set (α × α)) => compRel t 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 : Set (α × α)} (hs : s ∈ uniformity α) : ∀ᶠ (t : Set (α × α)) in (uniformity α).smallSets, compRel t 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 : Set (α × α)} (hV : IsOpen V) : IsOpen (ball x V)

theorem UniformSpace.isClosed_ball {α : Type ua} [UniformSpace α] (x : α) {V : Set (α × α)} (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 α ∧ SymmetricRel 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 : Set (α × α)) => {y : α | (y, a) ∈ s} ×ˢ {y : α | (b, y) ∈ s}

theorem nhdset_of_mem_uniformity {α : Type ua} [UniformSpace α] {d : Set (α × α)} (s : Set (α × α)) (hd : d ∈ uniformity α) : ∃ (t : Set (α × α)), 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 : ℕ → Set (α × α)), (uniformity α).HasAntitoneBasis V ∧ ∀ (n : ℕ), SymmetricRel (V n)

Closure and interior in uniform spaces

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

theorem uniformity_hasBasis_closed {α : Type ua} [UniformSpace α] : (uniformity α).HasBasis (fun (V : Set (α × α)) => 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 : ι → Set (α × α)} (h : (uniformity α).HasBasis p U) : (uniformity α).HasBasis p fun (i : ι) => closure (U i)

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

Closed entourages form a basis of the uniformity filter.

theorem closure_eq_inter_uniformity {α : Type ua} [UniformSpace α] {t : Set (α × α)} : closure t = ⋂ d ∈ uniformity α, compRel d (compRel t d)

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

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

theorem mem_uniformity_isClosed {α : Type ua} [UniformSpace α] {s : Set (α × α)} (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

@[deprecated isOpen_iff_isOpen_ball_subset (since := "2024-11-18")]

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

Alias of isOpen_iff_isOpen_ball_subset.

theorem Dense.biUnion_uniformity_ball {α : Type ua} [UniformSpace α] {s : Set α} {U : Set (α × α)} (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 : Set (α × α)} (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 : Set (α × α)) => 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 : β → Set (α × α)} (h : (uniformity α).HasBasis p s) {t : Set (α × α)} : 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 : Set (α × α)) => V ∈ uniformity α ∧ IsOpen V ∧ SymmetricRel V) id

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

theorem comp_open_symm_mem_uniformity_sets {α : Type ua} [UniformSpace α] {s : Set (α × α)} (hs : s ∈ uniformity α) : ∃ t ∈ uniformity α, IsOpen t ∧ SymmetricRel t ∧ compRel t t ⊆ s

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 α

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

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

Equations

• instTopUniformSpace = { top := UniformSpace.mk ⊤ ⋯ ⋯ ⋯ }

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

Equations

• instBotUniformSpace = { bot := UniformSpace.mk (Filter.principal idRel) ⋯ ⋯ ⋯ }

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

Equations

• instMinUniformSpace = { min := fun (u₁ u₂ : UniformSpace α) => UniformSpace.mk (uniformity α ⊓ uniformity α) ⋯ ⋯ ⋯ }

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

Equations

• instCompleteLatticeUniformSpace = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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 idRel

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

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

Equations

• inhabitedUniformSpace = { default := ⊥ }

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

Equations

• inhabitedUniformSpaceCore = { default := default.toCore }

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

• UniformSpace.comap f u = UniformSpace.mk (Filter.comap (fun (p : α × α) => (f p.1, f p.2)) (uniformity β)) ⋯ ⋯ ⋯

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 : Set (β × β)} {x : α} : UniformSpace.ball x (Prod.map f f ⁻¹' U) = f ⁻¹' UniformSpace.ball (f x) U

@[simp]

theorem uniformSpace_comap_id {α : Type u_2} : UniformSpace.comap id = 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_mono {α : Type u_2} {γ : Type u_3} {f : α → γ} : Monotone fun (u : UniformSpace γ) => comap f u

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

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

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₂) : toTopologicalSpace ≤ toTopologicalSpace

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

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

theorem Filter.HasBasis.uniformSpace_eq_bot {α : Type ua} {ι : Sort u_2} {p : ι → Prop} {s : ι → Set (α × α)} {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 α} : toTopologicalSpace = ⨅ (i : ι), toTopologicalSpace

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

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

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

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 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 idRel) : DiscreteTopology α

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

instance instUniformSpaceEmpty : UniformSpace Empty

Equations

• instUniformSpaceEmpty = ⊥

instance instUniformSpacePUnit : UniformSpace PUnit.{u_2 + 1}

Equations

• instUniformSpacePUnit = ⊥

instance instUniformSpaceBool : UniformSpace Bool

Equations

• instUniformSpaceBool = ⊥

instance instUniformSpaceNat : UniformSpace ℕ

Equations

• instUniformSpaceNat = ⊥

instance instUniformSpaceInt : UniformSpace ℤ

Equations

• instUniformSpaceInt = ⊥

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

Equations

• instUniformSpaceAdditive = inst✝

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 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 uniformContinuousOn_iff_restrict {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} {s : Set α} : UniformContinuousOn f s ↔ UniformContinuous (s.restrict f)

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 instUniformSpaceMulOpposite {α : Type ua} [UniformSpace α] : UniformSpace αᵐᵒᵖ

Equations

• instUniformSpaceMulOpposite = UniformSpace.comap MulOpposite.unop inst✝

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

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 : Set (β × β)} {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 : Set (α × α)) (v : Set (β × β)) : Set ((α × β) × α × β)

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 : Set (α × α)} {v : Set (β × β)} {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 : Set (α × α)} {v : Set (β × β)} (hu : u ∈ uniformity α) (hv : v ∈ uniformity β) : entourageProd u v ∈ uniformity (α × β)

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

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 → Set (α × α)} {sb : ιb → Set (β × β)} (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.prod_mk {α : 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.prod_mk_left {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {f : α × β → γ} (h : UniformContinuous f) (b : β) : UniformContinuous fun (a : α) => f (a, b)

theorem UniformContinuous.prod_mk_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)

@[deprecated UniformContinuous.prodMap (since := "2024-10-06")]

theorem UniformContinuous.prod_map {α : 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)

Alias of UniformContinuous.prodMap.

theorem toTopologicalSpace_prod {α : Type u_2} {β : Type u_3} [u : UniformSpace α] [v : UniformSpace β] : UniformSpace.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} : UniformSpace.toTopologicalSpace = instTopologicalSpaceSubtype

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 : Set (α × α)} (ha : a ∈ uniformity α) {b : Set (β × β)} (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 : Set (α × α)} {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)