Uniform spaces

Uniform spaces are a generalization of metric spaces and topological groups. Many concepts directly generalize to uniform spaces, e.g.

• uniform continuity (in this file)
• completeness (in Cauchy.lean)
• extension of uniform continuous functions to complete spaces (in IsUniformEmbedding.lean)
• totally bounded sets (in Cauchy.lean)
• totally bounded complete sets are compact (in Cauchy.lean)

A uniform structure on a type X is a filter 𝓤 X on X × X satisfying some conditions which makes it reasonable to say that ∀ᶠ (p : X × X) in 𝓤 X, ... means "for all p.1 and p.2 in X close enough, ...". Elements of this filter are called entourages of X. The two main examples are:

• If X is a metric space, V ∈ 𝓤 X ↔ ∃ ε > 0, { p | dist p.1 p.2 < ε } ⊆ V
• If G is an additive topological group, V ∈ 𝓤 G ↔ ∃ U ∈ 𝓝 (0 : G), {p | p.2 - p.1 ∈ U} ⊆ V

Those examples are generalizations in two different directions of the elementary example where X = ℝ and V ∈ 𝓤 ℝ ↔ ∃ ε > 0, { p | |p.2 - p.1| < ε } ⊆ V which features both the topological group structure on ℝ and its metric space structure.

Each uniform structure on X induces a topology on X characterized by

nhds_eq_comap_uniformity : ∀ {x : X}, 𝓝 x = comap (Prod.mk x) (𝓤 X)

where Prod.mk x : X → X × X := (fun y ↦ (x, y)) is the partial evaluation of the product constructor.

The dictionary with metric spaces includes:

• an upper bound for dist x y translates into (x, y) ∈ V for some V ∈ 𝓤 X
• a ball ball x r roughly corresponds to UniformSpace.ball x V := {y | (x, y) ∈ V} for some V ∈ 𝓤 X, but the later is more general (it includes in particular both open and closed balls for suitable V). In particular we have: isOpen_iff_ball_subset {s : Set X} : IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 X, ball x V ⊆ s

The triangle inequality is abstracted to a statement involving the composition of relations in X. First note that the triangle inequality in a metric space is equivalent to ∀ (x y z : X) (r r' : ℝ), dist x y ≤ r → dist y z ≤ r' → dist x z ≤ r + r'. Then, for any V and W with type Set (X × X), the composition V ○ W : Set (X × X) is defined as { p : X × X | ∃ z, (p.1, z) ∈ V ∧ (z, p.2) ∈ W }. In the metric space case, if V = { p | dist p.1 p.2 ≤ r } and W = { p | dist p.1 p.2 ≤ r' } then the triangle inequality, as reformulated above, says V ○ W is contained in {p | dist p.1 p.2 ≤ r + r'} which is the entourage associated to the radius r + r'. In general we have mem_ball_comp (h : y ∈ ball x V) (h' : z ∈ ball y W) : z ∈ ball x (V ○ W). Note that this discussion does not depend on any axiom imposed on the uniformity filter, it is simply captured by the definition of composition.

The uniform space axioms ask the filter 𝓤 X to satisfy the following:

• every V ∈ 𝓤 X contains the diagonal idRel = { p | p.1 = p.2 }. This abstracts the fact that dist x x ≤ r for every non-negative radius r in the metric space case and also that x - x belongs to every neighborhood of zero in the topological group case.
• V ∈ 𝓤 X → Prod.swap '' V ∈ 𝓤 X. This is tightly related the fact that dist x y = dist y x in a metric space, and to continuity of negation in the topological group case.
• ∀ V ∈ 𝓤 X, ∃ W ∈ 𝓤 X, W ○ W ⊆ V. In the metric space case, it corresponds to cutting the radius of a ball in half and applying the triangle inequality. In the topological group case, it comes from continuity of addition at (0, 0).

These three axioms are stated more abstractly in the definition below, in terms of operations on filters, without directly manipulating entourages.

Main definitions

• UniformSpace X is a uniform space structure on a type X
• UniformContinuous f is a predicate saying a function f : α → β between uniform spaces is uniformly continuous : ∀ r ∈ 𝓤 β, ∀ᶠ (x : α × α) in 𝓤 α, (f x.1, f x.2) ∈ r

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).

Implementation notes

There is already a theory of relations in Data/Rel.lean where the main definition is def Rel (α β : Type*) := α → β → Prop. The relations used in the current file involve only one type, but this is not the reason why we don't reuse Data/Rel.lean. We use Set (α × α) instead of Rel α α because we really need sets to use the filter library, and elements of filters on α × α have type Set (α × α).

The structure UniformSpace X bundles a uniform structure on X, a topology on X and an assumption saying those are compatible. This may not seem mathematically reasonable at first, but is in fact an instance of the forgetful inheritance pattern. See Note [forgetful inheritance] below.

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 Set (α × α)

def idRel {α : Type u_2} : Set (α × α)

The identity relation, or the graph of the identity function

Equations

• idRel = {p : α × α | p.1 = p.2}

@[simp]

theorem mem_idRel {α : Type ua} {a b : α} : (a, b) ∈ idRel ↔ a = b

@[simp]

theorem idRel_subset {α : Type ua} {s : Set (α × α)} : idRel ⊆ s ↔ ∀ (a : α), (a, a) ∈ s

theorem eq_singleton_left_of_prod_subset_idRel {X : Type u_2} {S T : Set X} (hS : S.Nonempty) (hT : T.Nonempty) (h_diag : S ×ˢ T ⊆ idRel) : ∃ (x : X), S = {x}

theorem eq_singleton_right_prod_subset_idRel {X : Type u_2} {S T : Set X} (hS : S.Nonempty) (hT : T.Nonempty) (h_diag : S ×ˢ T ⊆ idRel) : ∃ (x : X), T = {x}

theorem eq_singleton_prod_subset_idRel {X : Type u_2} {S T : Set X} (hS : S.Nonempty) (hT : T.Nonempty) (h_diag : S ×ˢ T ⊆ idRel) : ∃ (x : X), S = {x} ∧ T = {x}

def compRel {α : Type ua} (r₁ r₂ : Set (α × α)) : Set (α × α)

The composition of relations

Equations

• compRel r₁ r₂ = {p : α × α | ∃ (z : α), (p.1, z) ∈ r₁ ∧ (z, p.2) ∈ r₂}

def Uniformity.«term_○_» : Lean.TrailingParserDescr

The composition of relations

Equations

• Uniformity.«term_○_» = Lean.ParserDescr.trailingNode `Uniformity.«term_○_» 62 62 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ○ ") (Lean.ParserDescr.cat `term 63))

@[simp]

theorem mem_compRel {α : Type u} {r₁ r₂ : Set (α × α)} {x y : α} : (x, y) ∈ compRel r₁ r₂ ↔ ∃ (z : α), (x, z) ∈ r₁ ∧ (z, y) ∈ r₂

@[simp]

theorem swap_idRel {α : Type ua} : Prod.swap '' idRel = idRel

theorem Monotone.compRel {α : Type ua} {β : Type ub} [Preorder β] {f g : β → Set (α × α)} (hf : Monotone f) (hg : Monotone g) : Monotone fun (x : β) => _root_.compRel (f x) (g x)

theorem compRel_mono {α : Type ua} {f g h k : Set (α × α)} (h₁ : f ⊆ h) (h₂ : g ⊆ k) : compRel f g ⊆ compRel h k

theorem prod_mk_mem_compRel {α : Type ua} {a b c : α} {s t : Set (α × α)} (h₁ : (a, c) ∈ s) (h₂ : (c, b) ∈ t) : (a, b) ∈ compRel s t

@[simp]

theorem id_compRel {α : Type ua} {r : Set (α × α)} : compRel idRel r = r

theorem compRel_assoc {α : Type ua} {r s t : Set (α × α)} : compRel (compRel r s) t = compRel r (compRel s t)

theorem left_subset_compRel {α : Type ua} {s t : Set (α × α)} (h : idRel ⊆ t) : s ⊆ compRel s t

theorem right_subset_compRel {α : Type ua} {s t : Set (α × α)} (h : idRel ⊆ s) : t ⊆ compRel s t

theorem subset_comp_self {α : Type ua} {s : Set (α × α)} (h : idRel ⊆ s) : s ⊆ compRel s s

theorem subset_iterate_compRel {α : Type ua} {s t : Set (α × α)} (h : idRel ⊆ s) (n : ℕ) : t ⊆ (fun (x : Set (α × α)) => compRel s x)^[n] t

def IsSymmetricRel {α : Type ua} (V : Set (α × α)) : Prop

The relation is invariant under swapping factors.

Equations

• IsSymmetricRel V = (Prod.swap ⁻¹' V = V)

def symmetrizeRel {α : Type ua} (V : Set (α × α)) : Set (α × α)

The maximal symmetric relation contained in a given relation.

Equations

• symmetrizeRel V = V ∩ Prod.swap ⁻¹' V

theorem symmetric_symmetrizeRel {α : Type ua} (V : Set (α × α)) : IsSymmetricRel (symmetrizeRel V)

theorem symmetrizeRel_subset_self {α : Type ua} (V : Set (α × α)) : symmetrizeRel V ⊆ V

theorem symmetrize_mono {α : Type ua} {V W : Set (α × α)} (h : V ⊆ W) : symmetrizeRel V ⊆ symmetrizeRel W

theorem IsSymmetricRel.mk_mem_comm {α : Type ua} {V : Set (α × α)} (hV : IsSymmetricRel V) {x y : α} : (x, y) ∈ V ↔ (y, x) ∈ V

theorem IsSymmetricRel.eq {α : Type ua} {U : Set (α × α)} (hU : IsSymmetricRel U) : Prod.swap ⁻¹' U = U

theorem IsSymmetricRel.inter {α : Type ua} {U V : Set (α × α)} (hU : IsSymmetricRel U) (hV : IsSymmetricRel V) : IsSymmetricRel (U ∩ V)

structure UniformSpace.Core (α : Type u) : Type u

This core description of a uniform space is outside of the type class hierarchy. It is useful for constructions of uniform spaces, when the topology is derived from the uniform space.

• uniformity : Filter (α × α)

  The uniformity filter. Once UniformSpace is defined, 𝓤 α (_root_.uniformity) becomes the normal form.

• refl : Filter.principal idRel ≤ self.uniformity

  Every set in the uniformity filter includes the diagonal.

• symm : Filter.Tendsto Prod.swap self.uniformity self.uniformity

  If s ∈ uniformity, then Prod.swap ⁻¹' s ∈ uniformity.

• comp : (self.uniformity.lift' fun (s : Set (α × α)) => compRel s s) ≤ self.uniformity

  For every set u ∈ uniformity, there exists v ∈ uniformity such that v ○ v ⊆ u.

theorem UniformSpace.Core.comp_mem_uniformity_sets {α : Type ua} {c : Core α} {s : Set (α × α)} (hs : s ∈ c.uniformity) : ∃ t ∈ c.uniformity, compRel t t ⊆ s

def UniformSpace.Core.mk' {α : Type u} (U : Filter (α × α)) (refl : ∀ r ∈ U, ∀ (x : α), (x, x) ∈ r) (symm : ∀ r ∈ U, Prod.swap ⁻¹' r ∈ U) (comp : ∀ r ∈ U, ∃ t ∈ U, compRel t t ⊆ r) : Core α

An alternative constructor for UniformSpace.Core. This version unfolds various Filter-related definitions.

Equations

• UniformSpace.Core.mk' U refl symm comp = { uniformity := U, refl := ⋯, symm := symm, comp := ⋯ }

def UniformSpace.Core.mkOfBasis {α : Type u} (B : FilterBasis (α × α)) (refl : ∀ r ∈ B, ∀ (x : α), (x, x) ∈ r) (symm : ∀ r ∈ B, ∃ t ∈ B, t ⊆ Prod.swap ⁻¹' r) (comp : ∀ r ∈ B, ∃ t ∈ B, compRel t t ⊆ r) : Core α

Defining a UniformSpace.Core from a filter basis satisfying some uniformity-like axioms.

Equations

• UniformSpace.Core.mkOfBasis B refl symm comp = { uniformity := B.filter, refl := ⋯, symm := ⋯, comp := ⋯ }

def UniformSpace.Core.toTopologicalSpace {α : Type u} (u : Core α) : TopologicalSpace α

A uniform space generates a topological space

Equations

• u.toTopologicalSpace = TopologicalSpace.mkOfNhds fun (x : α) => Filter.comap (Prod.mk x) u.uniformity

theorem UniformSpace.Core.ext {α : Type ua} {u₁ u₂ : Core α} : u₁.uniformity = u₂.uniformity → u₁ = u₂

theorem UniformSpace.Core.nhds_toTopologicalSpace {α : Type u} (u : Core α) (x : α) : nhds x = Filter.comap (Prod.mk x) u.uniformity

class UniformSpace (α : Type u) extends TopologicalSpace α : Type u

A uniform space is a generalization of the "uniform" topological aspects of a metric space. It consists of a filter on α × α called the "uniformity", which satisfies properties analogous to the reflexivity, symmetry, and triangle properties of a metric.

A metric space has a natural uniformity, and a uniform space has a natural topology. A topological group also has a natural uniformity, even when it is not metrizable.

• IsOpen : Set α → Prop
• isOpen_univ : TopologicalSpace.IsOpen Set.univ
• isOpen_inter (s t : Set α) : TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
• isOpen_sUnion (s : Set (Set α)) : (∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
• uniformity : Filter (α × α)

  The uniformity filter.

• symm : Filter.Tendsto Prod.swap UniformSpace.uniformity UniformSpace.uniformity

  If s ∈ uniformity, then Prod.swap ⁻¹' s ∈ uniformity.

• comp : (UniformSpace.uniformity.lift' fun (s : Set (α × α)) => compRel s s) ≤ UniformSpace.uniformity

  For every set u ∈ uniformity, there exists v ∈ uniformity such that v ○ v ⊆ u.

• nhds_eq_comap_uniformity (x : α) : nhds x = Filter.comap (Prod.mk x) UniformSpace.uniformity

  The uniformity agrees with the topology: the neighborhoods filter of each point x is equal to Filter.comap (Prod.mk x) (𝓤 α).

def uniformity (α : Type u) [UniformSpace α] : Filter (α × α)

The uniformity is a filter on α × α (inferred from an ambient uniform space structure on α).

Equations

• uniformity α = UniformSpace.uniformity

def Uniformity.«term𝓤[_]» : Lean.ParserDescr

Notation for the uniformity filter with respect to a non-standard UniformSpace instance.

Equations

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

def Uniformity.term𝓤 : Lean.ParserDescr

The uniformity is a filter on α × α (inferred from an ambient uniform space structure on α).

Equations

• Uniformity.term𝓤 = Lean.ParserDescr.node `Uniformity.term𝓤 1024 (Lean.ParserDescr.symbol "𝓤")

@[reducible, inline]

abbrev UniformSpace.ofCoreEq {α : Type u} (u : Core α) (t : TopologicalSpace α) (h : t = u.toTopologicalSpace) : UniformSpace α

Construct a UniformSpace from a u : UniformSpace.Core and a TopologicalSpace structure that is equal to u.toTopologicalSpace.

Equations

• UniformSpace.ofCoreEq u t h = UniformSpace.mk u.uniformity ⋯ ⋯ ⋯

@[reducible, inline]

abbrev UniformSpace.ofCore {α : Type u} (u : Core α) : UniformSpace α

Construct a UniformSpace from a UniformSpace.Core.

Equations

• UniformSpace.ofCore u = UniformSpace.ofCoreEq u u.toTopologicalSpace ⋯

@[reducible, inline]

abbrev UniformSpace.toCore {α : Type ua} (u : UniformSpace α) : Core α

Construct a UniformSpace.Core from a UniformSpace.

Equations

• u.toCore = { uniformity := UniformSpace.uniformity, refl := ⋯, symm := ⋯, comp := ⋯ }

theorem UniformSpace.toCore_toTopologicalSpace {α : Type ua} (u : UniformSpace α) : u.toCore.toTopologicalSpace = toTopologicalSpace

theorem UniformSpace.ext {α : Type ua} {u₁ u₂ : UniformSpace α} (h : uniformity α = uniformity α) : u₁ = u₂

theorem UniformSpace.ext_iff {α : Type ua} {u₁ u₂ : UniformSpace α} : u₁ = u₂ ↔ ∀ (s : Set (α × α)), s ∈ uniformity α ↔ s ∈ uniformity α

theorem UniformSpace.ofCoreEq_toCore {α : Type ua} (u : UniformSpace α) (t : TopologicalSpace α) (h : t = u.toCore.toTopologicalSpace) : ofCoreEq u.toCore t h = u

@[reducible, inline]

abbrev UniformSpace.replaceTopology {α : Type u_2} [i : TopologicalSpace α] (u : UniformSpace α) (h : i = toTopologicalSpace) : UniformSpace α

Replace topology in a UniformSpace instance with a propositionally (but possibly not definitionally) equal one.

Equations

• u.replaceTopology h = UniformSpace.mk UniformSpace.uniformity ⋯ ⋯ ⋯

theorem UniformSpace.replaceTopology_eq {α : Type u_2} [i : TopologicalSpace α] (u : UniformSpace α) (h : i = toTopologicalSpace) : u.replaceTopology h = u

theorem nhds_eq_comap_uniformity {α : Type ua} [UniformSpace α] {x : α} : nhds x = Filter.comap (Prod.mk x) (uniformity α)

theorem isOpen_uniformity {α : Type ua} [UniformSpace α] {s : Set α} : IsOpen s ↔ ∀ x ∈ s, {p : α × α | p.1 = x → p.2 ∈ s} ∈ uniformity α

theorem refl_le_uniformity {α : Type ua} [UniformSpace α] : Filter.principal idRel ≤ uniformity α

instance uniformity.neBot {α : Type ua} [UniformSpace α] [Nonempty α] : (uniformity α).NeBot

theorem refl_mem_uniformity {α : Type ua} [UniformSpace α] {x : α} {s : Set (α × α)} (h : s ∈ uniformity α) : (x, x) ∈ s

theorem mem_uniformity_of_eq {α : Type ua} [UniformSpace α] {x y : α} {s : Set (α × α)} (h : s ∈ uniformity α) (hx : x = y) : (x, y) ∈ s

theorem symm_le_uniformity {α : Type ua} [UniformSpace α] : Filter.map Prod.swap (uniformity α) ≤ uniformity α

theorem comp_le_uniformity {α : Type ua} [UniformSpace α] : ((uniformity α).lift' fun (s : Set (α × α)) => compRel s s) ≤ uniformity α

theorem lift'_comp_uniformity {α : Type ua} [UniformSpace α] : ((uniformity α).lift' fun (s : Set (α × α)) => compRel s s) = uniformity α

theorem tendsto_swap_uniformity {α : Type ua} [UniformSpace α] : Filter.Tendsto Prod.swap (uniformity α) (uniformity α)

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

theorem Filter.Tendsto.uniformity_trans {α : Type ua} {β : Type ub} [UniformSpace α] {l : Filter β} {f₁ f₂ f₃ : β → α} (h₁₂ : Tendsto (fun (x : β) => (f₁ x, f₂ x)) l (uniformity α)) (h₂₃ : Tendsto (fun (x : β) => (f₂ x, f₃ x)) l (uniformity α)) : Tendsto (fun (x : β) => (f₁ x, f₃ x)) l (uniformity α)

Relation fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α) is transitive.

theorem Filter.Tendsto.uniformity_symm {α : Type ua} {β : Type ub} [UniformSpace α] {l : Filter β} {f : β → α × α} (h : Tendsto f l (uniformity α)) : Tendsto (fun (x : β) => ((f x).2, (f x).1)) l (uniformity α)

Relation fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α) is symmetric.

theorem tendsto_diag_uniformity {α : Type ua} {β : Type ub} [UniformSpace α] (f : β → α) (l : Filter β) : Filter.Tendsto (fun (x : β) => (f x, f x)) l (uniformity α)

Relation fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α) is reflexive.

theorem tendsto_const_uniformity {α : Type ua} {β : Type ub} [UniformSpace α] {a : α} {f : Filter β} : Filter.Tendsto (fun (x : β) => (a, a)) f (uniformity α)

theorem symm_of_uniformity {α : Type ua} [UniformSpace α] {s : Set (α × α)} (hs : s ∈ uniformity α) : ∃ t ∈ uniformity α, (∀ (a b : α), (a, b) ∈ t → (b, a) ∈ t) ∧ t ⊆ s

theorem comp_symm_of_uniformity {α : Type ua} [UniformSpace α] {s : Set (α × α)} (hs : s ∈ uniformity α) : ∃ t ∈ uniformity α, (∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t) ∧ compRel t t ⊆ s

theorem uniformity_le_symm {α : Type ua} [UniformSpace α] : uniformity α ≤ Prod.swap <$> uniformity α

theorem uniformity_eq_symm {α : Type ua} [UniformSpace α] : uniformity α = Prod.swap <$> uniformity α

@[simp]

theorem comap_swap_uniformity {α : Type ua} [UniformSpace α] : Filter.comap Prod.swap (uniformity α) = uniformity α

theorem symmetrize_mem_uniformity {α : Type ua} [UniformSpace α] {V : Set (α × α)} (h : V ∈ uniformity α) : symmetrizeRel V ∈ uniformity α

theorem UniformSpace.hasBasis_symmetric {α : Type ua} [UniformSpace α] : (uniformity α).HasBasis (fun (s : Set (α × α)) => s ∈ uniformity α ∧ IsSymmetricRel s) id

Symmetric entourages form a basis of 𝓤 α

theorem uniformity_lift_le_swap {α : Type ua} {β : Type ub} [UniformSpace α] {g : Set (α × α) → Filter β} {f : Filter β} (hg : Monotone g) (h : ((uniformity α).lift fun (s : Set (α × α)) => g (Prod.swap ⁻¹' s)) ≤ f) : (uniformity α).lift g ≤ f

theorem uniformity_lift_le_comp {α : Type ua} {β : Type ub} [UniformSpace α] {f : Set (α × α) → Filter β} (h : Monotone f) : ((uniformity α).lift fun (s : Set (α × α)) => f (compRel s s)) ≤ (uniformity α).lift f

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

theorem comp_le_uniformity3 {α : Type ua} [UniformSpace α] : ((uniformity α).lift' fun (s : Set (α × α)) => compRel s (compRel s s)) ≤ uniformity α

See also comp3_mem_uniformity.

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

See also comp_open_symm_mem_uniformity_sets.

theorem subset_comp_self_of_mem_uniformity {α : Type ua} [UniformSpace α] {s : Set (α × α)} (h : s ∈ uniformity α) : s ⊆ compRel s s

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

Balls in uniform spaces

def UniformSpace.ball {β : Type ub} (x : β) (V : Set (β × β)) : Set β

The ball around (x : β) with respect to (V : Set (β × β)). Intended to be used for V ∈ 𝓤 β, but this is not needed for the definition. Recovers the notions of metric space ball when V = {p | dist p.1 p.2 < r }.

Equations

• UniformSpace.ball x V = Prod.mk x ⁻¹' V

theorem UniformSpace.mem_ball_self {α : Type ua} [UniformSpace α] (x : α) {V : Set (α × α)} : V ∈ uniformity α → x ∈ ball x V

theorem UniformSpace.mem_ball_comp {β : Type ub} {V W : Set (β × β)} {x y z : β} (h : y ∈ ball x V) (h' : z ∈ ball y W) : z ∈ ball x (compRel V W)

The triangle inequality for UniformSpace.ball

theorem UniformSpace.ball_subset_of_comp_subset {β : Type ub} {V W : Set (β × β)} {x y : β} (h : x ∈ ball y W) (h' : compRel W W ⊆ V) : ball x W ⊆ ball y V

theorem UniformSpace.ball_mono {β : Type ub} {V W : Set (β × β)} (h : V ⊆ W) (x : β) : ball x V ⊆ ball x W

theorem UniformSpace.ball_inter {β : Type ub} (x : β) (V W : Set (β × β)) : ball x (V ∩ W) = ball x V ∩ ball x W

theorem UniformSpace.ball_inter_left {β : Type ub} (x : β) (V W : Set (β × β)) : ball x (V ∩ W) ⊆ ball x V

theorem UniformSpace.ball_inter_right {β : Type ub} (x : β) (V W : Set (β × β)) : ball x (V ∩ W) ⊆ ball x W

theorem UniformSpace.mem_ball_symmetry {β : Type ub} {V : Set (β × β)} (hV : IsSymmetricRel V) {x y : β} : x ∈ ball y V ↔ y ∈ ball x V

theorem UniformSpace.ball_eq_of_symmetry {β : Type ub} {V : Set (β × β)} (hV : IsSymmetricRel V) {x : β} : ball x V = {y : β | (y, x) ∈ V}

theorem UniformSpace.mem_comp_of_mem_ball {β : Type ub} {V W : Set (β × β)} {x y z : β} (hV : IsSymmetricRel V) (hx : x ∈ ball z V) (hy : y ∈ ball z W) : (x, y) ∈ compRel V W

theorem UniformSpace.mem_comp_comp {β : Type ub} {V W M : Set (β × β)} (hW' : IsSymmetricRel W) {p : β × β} : p ∈ compRel (compRel V M) W ↔ (ball p.1 V ×ˢ ball p.2 W ∩ M).Nonempty

Neighborhoods in uniform spaces

theorem mem_nhds_uniformity_iff_right {α : Type ua} [UniformSpace α] {x : α} {s : Set α} : s ∈ nhds x ↔ {p : α × α | p.1 = x → p.2 ∈ s} ∈ uniformity α

theorem mem_nhds_uniformity_iff_left {α : Type ua} [UniformSpace α] {x : α} {s : Set α} : s ∈ nhds x ↔ {p : α × α | p.2 = x → p.1 ∈ s} ∈ uniformity α

theorem nhdsWithin_eq_comap_uniformity_of_mem {α : Type ua} [UniformSpace α] {x : α} {T : Set α} (hx : x ∈ T) (S : Set α) : nhdsWithin x S = Filter.comap (Prod.mk x) (uniformity α ⊓ Filter.principal (T ×ˢ S))

theorem nhdsWithin_eq_comap_uniformity {α : Type ua} [UniformSpace α] {x : α} (S : Set α) : nhdsWithin x S = Filter.comap (Prod.mk x) (uniformity α ⊓ Filter.principal (Set.univ ×ˢ S))

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

See also isOpen_iff_isOpen_ball_subset.

theorem nhds_basis_uniformity' {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ι → Prop} {s : ι → Set (α × α)} (h : (uniformity α).HasBasis p s) {x : α} : (nhds x).HasBasis p fun (i : ι) => UniformSpace.ball x (s i)

theorem nhds_basis_uniformity {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ι → Prop} {s : ι → Set (α × α)} (h : (uniformity α).HasBasis p s) {x : α} : (nhds x).HasBasis p fun (i : ι) => {y : α | (y, x) ∈ s i}

theorem nhds_eq_comap_uniformity' {α : Type ua} [UniformSpace α] {x : α} : nhds x = Filter.comap (fun (y : α) => (y, x)) (uniformity α)

theorem UniformSpace.mem_nhds_iff {α : Type ua} [UniformSpace α] {x : α} {s : Set α} : s ∈ nhds x ↔ ∃ V ∈ uniformity α, ball x V ⊆ s

theorem UniformSpace.ball_mem_nhds {α : Type ua} [UniformSpace α] (x : α) ⦃V : Set (α × α)⦄ (V_in : V ∈ uniformity α) : ball x V ∈ nhds x

theorem UniformSpace.ball_mem_nhdsWithin {α : Type ua} [UniformSpace α] {x : α} {S : Set α} ⦃V : Set (α × α)⦄ (x_in : x ∈ S) (V_in : V ∈ uniformity α ⊓ Filter.principal (S ×ˢ S)) : ball x V ∈ nhdsWithin x S

theorem UniformSpace.mem_nhds_iff_symm {α : Type ua} [UniformSpace α] {x : α} {s : Set α} : s ∈ nhds x ↔ ∃ V ∈ uniformity α, IsSymmetricRel V ∧ ball x V ⊆ s

theorem UniformSpace.hasBasis_nhds {α : Type ua} [UniformSpace α] (x : α) : (nhds x).HasBasis (fun (s : Set (α × α)) => s ∈ uniformity α ∧ IsSymmetricRel s) fun (s : Set (α × α)) => ball x s

theorem UniformSpace.mem_closure_iff_symm_ball {α : Type ua} [UniformSpace α] {s : Set α} {x : α} : x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ uniformity α → IsSymmetricRel V → (s ∩ ball x V).Nonempty

theorem UniformSpace.mem_closure_iff_ball {α : Type ua} [UniformSpace α] {s : Set α} {x : α} : x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ uniformity α → (ball x V ∩ s).Nonempty

theorem nhds_eq_uniformity {α : Type ua} [UniformSpace α] {x : α} : nhds x = (uniformity α).lift' (UniformSpace.ball x)

theorem nhds_eq_uniformity' {α : Type ua} [UniformSpace α] {x : α} : nhds x = (uniformity α).lift' fun (s : Set (α × α)) => {y : α | (y, x) ∈ s}

theorem mem_nhds_left {α : Type ua} [UniformSpace α] (x : α) {s : Set (α × α)} (h : s ∈ uniformity α) : {y : α | (x, y) ∈ s} ∈ nhds x

theorem mem_nhds_right {α : Type ua} [UniformSpace α] (y : α) {s : Set (α × α)} (h : s ∈ uniformity α) : {x : α | (x, y) ∈ s} ∈ nhds y

theorem exists_mem_nhds_ball_subset_of_mem_nhds {α : Type ua} [UniformSpace α] {a : α} {U : Set α} (h : U ∈ nhds a) : ∃ V ∈ nhds a, ∃ t ∈ uniformity α, ∀ a' ∈ V, UniformSpace.ball a' t ⊆ U

theorem tendsto_right_nhds_uniformity {α : Type ua} [UniformSpace α] {a : α} : Filter.Tendsto (fun (a' : α) => (a', a)) (nhds a) (uniformity α)

theorem tendsto_left_nhds_uniformity {α : Type ua} [UniformSpace α] {a : α} : Filter.Tendsto (fun (a' : α) => (a, a')) (nhds a) (uniformity α)

theorem lift_nhds_left {α : Type ua} {β : Type ub} [UniformSpace α] {x : α} {g : Set α → Filter β} (hg : Monotone g) : (nhds x).lift g = (uniformity α).lift fun (s : Set (α × α)) => g (UniformSpace.ball x s)

theorem lift_nhds_right {α : Type ua} {β : Type ub} [UniformSpace α] {x : α} {g : Set α → Filter β} (hg : Monotone g) : (nhds x).lift g = (uniformity α).lift fun (s : Set (α × α)) => g {y : α | (y, x) ∈ s}

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

theorem Filter.HasBasis.biInter_biUnion_ball {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ι → Prop} {U : ι → Set (α × α)} (h : (uniformity α).HasBasis p U) (s : Set α) : ⋂ (i : ι), ⋂ (_ : p i), ⋃ x ∈ s, UniformSpace.ball x (U i) = closure s

Uniform continuity

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

A function f : α → β is uniformly continuous if (f x, f y) tends to the diagonal as (x, y) tends to the diagonal. In other words, if x is sufficiently close to y, then f x is close to f y no matter where x and y are located in α.

Equations

• UniformContinuous f = Filter.Tendsto (fun (x : α × α) => (f x.1, f x.2)) (uniformity α) (uniformity β)

def Uniformity.«termUniformContinuous[_,_]» : Lean.ParserDescr

Notation for uniform continuity with respect to non-standard UniformSpace instances.

Equations

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

def UniformContinuousOn {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] (f : α → β) (s : Set α) : Prop

A function f : α → β is uniformly continuous on s : Set α if (f x, f y) tends to the diagonal as (x, y) tends to the diagonal while remaining in s ×ˢ s. In other words, if x is sufficiently close to y, then f x is close to f y no matter where x and y are located in s.

Equations

• UniformContinuousOn f s = Filter.Tendsto (fun (x : α × α) => (f x.1, f x.2)) (uniformity α ⊓ Filter.principal (s ×ˢ s)) (uniformity β)

theorem uniformContinuous_def {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} : UniformContinuous f ↔ ∀ r ∈ uniformity β, {x : α × α | (f x.1, f x.2) ∈ r} ∈ uniformity α

theorem uniformContinuous_iff_eventually {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} : UniformContinuous f ↔ ∀ r ∈ uniformity β, ∀ᶠ (x : α × α) in uniformity α, (f x.1, f x.2) ∈ r

theorem uniformContinuousOn_univ {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} : UniformContinuousOn f Set.univ ↔ UniformContinuous f

theorem uniformContinuous_of_const {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {c : α → β} (h : ∀ (a b : α), c a = c b) : UniformContinuous c

theorem uniformContinuous_id {α : Type ua} [UniformSpace α] : UniformContinuous id

theorem uniformContinuous_const {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {b : β} : UniformContinuous fun (x : α) => b

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

theorem UniformContinuous.iterate {β : Type ub} [UniformSpace β] (T : β → β) (n : ℕ) (h : UniformContinuous T) : UniformContinuous T^[n]

If a function T is uniformly continuous in a uniform space β, then its n-th iterate T^[n] is also uniformly continuous.

theorem Filter.HasBasis.uniformContinuous_iff {α : Type ua} {β : Type ub} {ι : Sort u_1} [UniformSpace α] {ι' : Sort u_2} [UniformSpace β] {p : ι → Prop} {s : ι → Set (α × α)} (ha : (uniformity α).HasBasis p s) {q : ι' → Prop} {t : ι' → Set (β × β)} (hb : (uniformity β).HasBasis q t) {f : α → β} : UniformContinuous f ↔ ∀ (i : ι'), q i → ∃ (j : ι), p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ t i

theorem Filter.HasBasis.uniformContinuousOn_iff {α : Type ua} {β : Type ub} {ι : Sort u_1} [UniformSpace α] {ι' : Sort u_2} [UniformSpace β] {p : ι → Prop} {s : ι → Set (α × α)} (ha : (uniformity α).HasBasis p s) {q : ι' → Prop} {t : ι' → Set (β × β)} (hb : (uniformity β).HasBasis q t) {f : α → β} {S : Set α} : UniformContinuousOn f S ↔ ∀ (i : ι'), q i → ∃ (j : ι), p j ∧ ∀ x ∈ S, ∀ y ∈ S, (x, y) ∈ s j → (f x, f y) ∈ t i