# 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`

## Notation #

Localized in `Uniformity`, we have the notation `𝓤 X` for the uniformity on a uniform space `X`. This file also uses a lot the notation `○` for composition of relations, seen as terms with type `SetRel X X`. This notation (defined in the file `Mathlib/Data/Rel.lean`) is localized in `SetRel`.

## Implementation notes #

We use the theory of relations as sets developed in `Mathlib/Data/Rel.lean`. The relevant definition is `SetRel X X := Set (X × X)`, which is the type of elements of the uniformity filter `𝓤 X : Filter (X × X)`.

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 `SetRel α α` #

source
@[deprecated SetRel.id (since := "2025-10-17")]
def idRel {α : Type u_2} :
Set (α × α)

The identity relation, or the graph of the identity function

Equations

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

Instances For

source
@[deprecated SetRel.mem_id (since := "2025-10-17")]
theorem mem_idRel {α : Type ua} {a b : α} :
(a, b) ∈ idRel ↔ a = b
source
@[deprecated SetRel.id_subset_iff (since := "2025-10-17")]
theorem idRel_subset {α : Type ua} {s : SetRel α α} :
idRel ⊆ s ↔ ∀ (a : α), (a, a) ∈ s
source
@[deprecated SetRel.exists_eq_singleton_of_prod_subset_id (since := "2025-10-17")]
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 ⊆ SetRel.id) :
∃ (x : X), S = {x}
source
@[deprecated SetRel.exists_eq_singleton_of_prod_subset_id (since := "2025-10-17")]
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 ⊆ SetRel.id) :
∃ (x : X), T = {x}
source
@[deprecated SetRel.exists_eq_singleton_of_prod_subset_id (since := "2025-10-17")]
theorem eq_singleton_prod_subset_idRel {α : Type u_1} {s t : Set α} (hs : s.Nonempty) (ht : t.Nonempty) (hst : s ×ˢ t ⊆ SetRel.id) :
∃ (x : α), s = {x} ∧ t = {x}

Alias of `SetRel.exists_eq_singleton_of_prod_subset_id`.

source
@[deprecated SetRel.comp (since := "2025-10-17")]
def compRel {α : Type ua} (r₁ r₂ : SetRel α α) :
Set (α × α)

The composition of relations

Equations

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

Instances For

source
@[deprecated SetRel.mem_comp (since := "2025-10-17")]
theorem mem_compRel {α : Type u} {r₁ r₂ : SetRel α α} {x y : α} :
(x, y) ∈ r₁.comp r₂ ↔ ∃ (z : α), (x, z) ∈ r₁ ∧ (z, y) ∈ r₂
source
@[deprecated SetRel.inv_id (since := "2025-10-17")]
theorem swap_idRel {α : Type ua} :
Prod.swap '' idRel = idRel
source
@[deprecated Monotone.relComp (since := "2025-10-17")]
theorem Monotone.compRel {α : Type ua} {β : Type ub} [Preorder β] {f g : β → SetRel α α} (hf : Monotone f) (hg : Monotone g) :
Monotone fun (x : β) => (f x).comp (g x)
source
@[deprecated SetRel.comp_subset_comp (since := "2025-10-17")]
theorem compRel_mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R₁ R₂ : SetRel α β} {S₁ S₂ : SetRel β γ} (hR : R₁ ⊆ R₂) (hS : S₁ ⊆ S₂) :
R₁.comp S₁ ⊆ R₂.comp S₂

Alias of `SetRel.comp_subset_comp`.

source
@[deprecated SetRel.comp_subset_comp_left (since := "2025-10-17")]
theorem compRel_left_mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R₁ R₂ : SetRel α β} {S : SetRel β γ} (hR : R₁ ⊆ R₂) :
R₁.comp S ⊆ R₂.comp S

Alias of `SetRel.comp_subset_comp_left`.

source
@[deprecated SetRel.comp_subset_comp_right (since := "2025-10-17")]
theorem compRel_right_mono {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : SetRel α β} {S₁ S₂ : SetRel β γ} (hS : S₁ ⊆ S₂) :
R.comp S₁ ⊆ R.comp S₂

Alias of `SetRel.comp_subset_comp_right`.

source
@[deprecated SetRel.prodMk_mem_comp (since := "2025-10-17")]
theorem prodMk_mem_compRel {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : SetRel α β} {S : SetRel β γ} {a : α} {b : β} {c : γ} (hab : (a, b) ∈ R) (hbc : (b, c) ∈ S) :
(a, c) ∈ R.comp S

Alias of `SetRel.prodMk_mem_comp`.

source
@[deprecated SetRel.prodMk_mem_comp (since := "2025-03-10")]
theorem prod_mk_mem_compRel {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : SetRel α β} {S : SetRel β γ} {a : α} {b : β} {c : γ} (hab : (a, b) ∈ R) (hbc : (b, c) ∈ S) :
(a, c) ∈ R.comp S

Alias of `SetRel.prodMk_mem_comp`.

source
@[deprecated SetRel.id_comp (since := "2025-10-17")]
theorem id_compRel {α : Type ua} {r : SetRel α α} :
SetRel.comp idRel r = r
source
@[deprecated SetRel.comp_assoc (since := "2025-10-17")]
theorem compRel_assoc {α : Type ua} {r s t : SetRel α α} :
(r.comp s).comp t = r.comp (s.comp t)
source
@[deprecated SetRel.left_subset_comp (since := "2025-10-17")]
theorem left_subset_compRel {α : Type ua} {s t : SetRel α α} (h : idRel ⊆ t) :
s ⊆ s.comp t
source
@[deprecated SetRel.right_subset_comp (since := "2025-10-17")]
theorem right_subset_compRel {α : Type ua} {s t : SetRel α α} (h : idRel ⊆ s) :
t ⊆ s.comp t
source
@[deprecated SetRel.left_subset_comp (since := "2025-10-17")]
theorem subset_comp_self {α : Type ua} {s : SetRel α α} (h : idRel ⊆ s) :
s ⊆ s.comp s
source
@[deprecated SetRel.subset_iterate_comp (since := "2025-10-17")]
theorem subset_iterate_compRel {α : Type ua} {s t : SetRel α α} (h : idRel ⊆ s) (n : ℕ) :
t ⊆ (fun (x : SetRel α α) => s.comp x)^[n] t
source
@[deprecated SetRel.IsSymm (since := "2025-10-17")]
def IsSymmetricRel {α : Type ua} (V : SetRel α α) :
Prop

The relation is invariant under swapping factors.

Equations

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

Instances For

source
@[deprecated SetRel.symmetrize (since := "2025-10-17")]
def symmetrizeRel {α : Type ua} (V : SetRel α α) :
SetRel α α

The maximal symmetric relation contained in a given relation.

Equations

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

Instances For

source
@[deprecated SetRel.isSymm_symmetrize (since := "2025-10-17")]
theorem symmetric_symmetrizeRel {α : Type ua} (V : SetRel α α) :
IsSymmetricRel (symmetrizeRel V)
source
@[deprecated SetRel.symmetrize_subset_self (since := "2025-10-17")]
theorem symmetrizeRel_subset_self {α : Type ua} (V : SetRel α α) :
symmetrizeRel V ⊆ V
source
@[deprecated SetRel.symmetrize_mono (since := "2025-10-17")]
theorem symmetrize_mono {α : Type ua} {V W : SetRel α α} (h : V ⊆ W) :
symmetrizeRel V ⊆ symmetrizeRel W
source
@[deprecated SetRel.comm (since := "2025-10-17")]
theorem IsSymmetricRel.mk_mem_comm {α : Type ua} {V : SetRel α α} (hV : IsSymmetricRel V) {x y : α} :
(x, y) ∈ V ↔ (y, x) ∈ V
source
@[deprecated SetRel.inv_eq_self (since := "2025-10-17")]
theorem IsSymmetricRel.eq {α : Type ua} {U : SetRel α α} (hU : IsSymmetricRel U) :
Prod.swap ⁻¹' U = U
source
@[deprecated SetRel.isSymm_inter (since := "2025-10-17")]
theorem IsSymmetricRel.inter {α : Type ua} {U V : SetRel α α} (hU : IsSymmetricRel U) (hV : IsSymmetricRel V) :
IsSymmetricRel (U ∩ V)
source
@[deprecated SetRel.isSymm_iInter (since := "2025-10-17")]
theorem IsSymmetricRel.iInter {α : Type ua} {ι : Sort u_1} {U : ι → SetRel α α} (hU : ∀ (i : ι), IsSymmetricRel (U i)) :
IsSymmetricRel (⋂ (i : ι), U i)
source
@[deprecated SetRel.IsSymm.sInter (since := "2025-10-17")]
theorem IsSymmetricRel.sInter {α : Type ua} {s : Set (SetRel α α)} (h : ∀ i ∈ s, IsSymmetricRel i) :
IsSymmetricRel (⋂₀ s)
source
@[deprecated SetRel.isSymm_id (since := "2025-10-17")]
theorem isSymmetricRel_idRel {α : Type ua} :
IsSymmetricRel idRel
source
@[deprecated SetRel.isSymm_univ (since := "2025-10-17")]
theorem isSymmetricRel_univ {α : Type ua} :
IsSymmetricRel Set.univ
source
@[deprecated SetRel.isSymm_preimage (since := "2025-10-17")]
theorem IsSymmetricRel.preimage_prodMap {α : Type ua} {β : Type ub} {U : Set (β × β)} (ht : IsSymmetricRel U) (f : α → β) :
IsSymmetricRel (Prod.map f f ⁻¹' U)
source
@[deprecated SetRel.isSymm_image (since := "2025-10-17")]
theorem IsSymmetricRel.image_prodMap {α : Type ua} {β : Type ub} {U : Set (α × α)} (ht : IsSymmetricRel U) (f : α → β) :
IsSymmetricRel (Prod.map f f '' U)
source
@[deprecated SetRel.prod_subset_comm (since := "2025-10-17")]
theorem IsSymmetricRel.prod_subset_comm {α : Type ua} {s : Set (α × α)} {t u : Set α} (hs : IsSymmetricRel s) :
t ×ˢ u ⊆ s ↔ u ×ˢ t ⊆ s
source
theorem SetRel.mem_filter_prod_comm {α : Type ua} (R : SetRel α α) {f g : Filter α} [R.IsSymm] :
R ∈ f ×ˢ g ↔ R ∈ g ×ˢ f
source
@[deprecated SetRel.mem_filter_prod_comm (since := "2025-10-17")]
theorem IsSymmetricRel.mem_filter_prod_comm {α : Type ua} {s : Set (α × α)} {f g : Filter α} (hs : IsSymmetricRel s) :
s ∈ f ×ˢ g ↔ s ∈ g ×ˢ f
source
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 SetRel.id ≤ 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 (α × α)) => SetRel.comp s s) ≤ self.uniformity

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

Instances For

source
theorem UniformSpace.Core.comp_mem_uniformity_sets {α : Type ua} {c : Core α} {s : SetRel α α} (hs : s ∈ c.uniformity) :
∃ t ∈ c.uniformity, SetRel.comp t t ⊆ s
source
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, SetRel.comp 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 := ⋯ }

Instances For

source
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, SetRel.comp 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 := ⋯ }

Instances For

source
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

Instances For

source
theorem UniformSpace.Core.ext {α : Type ua} {u₁ u₂ : Core α} :
u₁.uniformity = u₂.uniformity → u₁ = u₂
source
theorem UniformSpace.Core.nhds_toTopologicalSpace {α : Type u} (u : Core α) (x : α) :
nhds x = Filter.comap (Prod.mk x) u.uniformity
source
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 (α × α)) => SetRel.comp 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) (𝓤 α)`.

Instances

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

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

Equations

- uniformity α = UniformSpace.uniformity

Instances For

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

Instances For

source
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 "𝓤")

Instances For

source
@[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 = { toTopologicalSpace := t, uniformity := u.uniformity, symm := ⋯, comp := ⋯, nhds_eq_comap_uniformity := ⋯ }

Instances For

source
@[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 ⋯

Instances For

source
@[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 := ⋯ }

Instances For

source
theorem UniformSpace.toCore_toTopologicalSpace {α : Type ua} (u : UniformSpace α) :
u.toCore.toTopologicalSpace = u.toTopologicalSpace
source
theorem UniformSpace.mem_uniformity_ofCore_iff {α : Type ua} {u : Core α} {s : SetRel α α} :
s ∈ uniformity α ↔ s ∈ u.uniformity
source
theorem UniformSpace.ext {α : Type ua} {u₁ u₂ : UniformSpace α} (h : uniformity α = uniformity α) :
u₁ = u₂
source
theorem UniformSpace.ext_iff {α : Type ua} {u₁ u₂ : UniformSpace α} :
u₁ = u₂ ↔ ∀ (s : Set (α × α)), s ∈ uniformity α ↔ s ∈ uniformity α
source
theorem UniformSpace.ofCoreEq_toCore {α : Type ua} (u : UniformSpace α) (t : TopologicalSpace α) (h : t = u.toCore.toTopologicalSpace) :
ofCoreEq u.toCore t h = u
source
@[reducible, inline]
abbrev UniformSpace.replaceTopology {α : Type u_2} [i : TopologicalSpace α] (u : UniformSpace α) (h : i = u.toTopologicalSpace) :
UniformSpace α

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

Equations

- u.replaceTopology h = { toTopologicalSpace := i, uniformity := UniformSpace.uniformity, symm := ⋯, comp := ⋯, nhds_eq_comap_uniformity := ⋯ }

Instances For

source
theorem UniformSpace.replaceTopology_eq {α : Type u_2} [i : TopologicalSpace α] (u : UniformSpace α) (h : i = u.toTopologicalSpace) :
u.replaceTopology h = u
source
theorem nhds_eq_comap_uniformity {α : Type ua} [UniformSpace α] {x : α} :
nhds x = Filter.comap (Prod.mk x) (uniformity α)
source
theorem isOpen_uniformity {α : Type ua} [UniformSpace α] {s : Set α} :
IsOpen s ↔ ∀ x ∈ s, {p : α × α | p.1 = x → p.2 ∈ s} ∈ uniformity α
source
theorem refl_le_uniformity {α : Type ua} [UniformSpace α] :
Filter.principal SetRel.id ≤ uniformity α
source
instance uniformity.neBot {α : Type ua} [UniformSpace α] [Nonempty α] :
(uniformity α).NeBot
source
theorem refl_mem_uniformity {α : Type ua} [UniformSpace α] {x : α} {s : SetRel α α} (h : s ∈ uniformity α) :
(x, x) ∈ s
source
theorem mem_uniformity_of_eq {α : Type ua} [UniformSpace α] {x y : α} {s : SetRel α α} (h : s ∈ uniformity α) (hx : x = y) :
(x, y) ∈ s
source
theorem symm_le_uniformity {α : Type ua} [UniformSpace α] :
Filter.map Prod.swap (uniformity α) ≤ uniformity α
source
theorem comp_le_uniformity {α : Type ua} [UniformSpace α] :
((uniformity α).lift' fun (s : SetRel α α) => s.comp s) ≤ uniformity α
source
theorem lift'_comp_uniformity {α : Type ua} [UniformSpace α] :
((uniformity α).lift' fun (s : SetRel α α) => s.comp s) = uniformity α
source
theorem tendsto_swap_uniformity {α : Type ua} [UniformSpace α] :
Filter.Tendsto Prod.swap (uniformity α) (uniformity α)
source
theorem comp_mem_uniformity_sets {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) :
∃ t ∈ uniformity α, SetRel.comp t t ⊆ s
source
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.

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

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

source
theorem tendsto_const_uniformity {α : Type ua} {β : Type ub} [UniformSpace α] {a : α} {f : Filter β} :
Filter.Tendsto (fun (x : β) => (a, a)) f (uniformity α)
source
theorem symm_of_uniformity {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) :
∃ t ∈ uniformity α, (∀ (a b : α), (a, b) ∈ t → (b, a) ∈ t) ∧ t ⊆ s
source
theorem comp_symm_of_uniformity {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) :
∃ t ∈ uniformity α, (∀ {a b : α}, (a, b) ∈ t → (b, a) ∈ t) ∧ SetRel.comp t t ⊆ s
source
theorem uniformity_le_symm {α : Type ua} [UniformSpace α] :
uniformity α ≤ Filter.map Prod.swap (uniformity α)
source
theorem uniformity_eq_symm {α : Type ua} [UniformSpace α] :
uniformity α = Filter.map Prod.swap (uniformity α)
source
@[simp]
theorem comap_swap_uniformity {α : Type ua} [UniformSpace α] :
Filter.comap Prod.swap (uniformity α) = uniformity α
source
theorem symmetrize_mem_uniformity {α : Type ua} [UniformSpace α] {V : SetRel α α} (h : V ∈ uniformity α) :
V.symmetrize ∈ uniformity α
source
theorem UniformSpace.hasBasis_symmetric {α : Type ua} [UniformSpace α] :
(uniformity α).HasBasis (fun (s : SetRel α α) => s ∈ uniformity α ∧ s.IsSymm) id

Symmetric entourages form a basis of `𝓤 α`

source
theorem uniformity_lift_le_swap {α : Type ua} {β : Type ub} [UniformSpace α] {g : SetRel α α → Filter β} {f : Filter β} (hg : Monotone g) (h : ((uniformity α).lift fun (s : Set (α × α)) => g (Prod.swap ⁻¹' s)) ≤ f) :
(uniformity α).lift g ≤ f
source
theorem uniformity_lift_le_comp {α : Type ua} {β : Type ub} [UniformSpace α] {f : SetRel α α → Filter β} (h : Monotone f) :
((uniformity α).lift fun (s : Set (α × α)) => f (SetRel.comp s s)) ≤ (uniformity α).lift f
source
theorem comp3_mem_uniformity {α : Type ua} [UniformSpace α] {s : SetRel α α} (hs : s ∈ uniformity α) :
∃ t ∈ uniformity α, SetRel.comp t (SetRel.comp t t) ⊆ s
source
theorem comp_le_uniformity3 {α : Type ua} [UniformSpace α] :
((uniformity α).lift' fun (s : SetRel α α) => s.comp (s.comp s)) ≤ uniformity α

See also `comp3_mem_uniformity`.

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

See also `comp_open_symm_mem_uniformity_sets`.

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

### Balls in uniform spaces #

source
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

Instances For

source
theorem UniformSpace.mem_ball_self {α : Type ua} [UniformSpace α] (x : α) {V : SetRel α α} :
V ∈ uniformity α → x ∈ ball x V
source
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 (SetRel.comp V W)

The triangle inequality for `UniformSpace.ball`

source
theorem UniformSpace.ball_subset_of_comp_subset {β : Type ub} {V W : Set (β × β)} {x y : β} (h : x ∈ ball y W) (h' : SetRel.comp W W ⊆ V) :
ball x W ⊆ ball y V
source
theorem UniformSpace.ball_mono {β : Type ub} {V W : Set (β × β)} (h : V ⊆ W) (x : β) :
ball x V ⊆ ball x W
source
theorem UniformSpace.ball_inter {β : Type ub} (x : β) (V W : Set (β × β)) :
ball x (V ∩ W) = ball x V ∩ ball x W
source
theorem UniformSpace.ball_inter_left {β : Type ub} (x : β) (V W : Set (β × β)) :
ball x (V ∩ W) ⊆ ball x V
source
theorem UniformSpace.ball_inter_right {β : Type ub} (x : β) (V W : Set (β × β)) :
ball x (V ∩ W) ⊆ ball x W
source
theorem UniformSpace.ball_iInter {β : Type ub} {ι : Sort u_1} {x : β} {V : ι → Set (β × β)} :
ball x (⋂ (i : ι), V i) = ⋂ (i : ι), ball x (V i)
source
theorem UniformSpace.mem_ball_symmetry {β : Type ub} {V : SetRel β β} [V.IsSymm] {x y : β} :
x ∈ ball y V ↔ y ∈ ball x V
source
theorem UniformSpace.ball_eq_of_symmetry {β : Type ub} {V : SetRel β β} [V.IsSymm] {x : β} :
ball x V = {y : β | (y, x) ∈ V}
source
theorem UniformSpace.mem_comp_of_mem_ball {β : Type ub} {V W : SetRel β β} {x y z : β} [V.IsSymm] (hx : x ∈ ball z V) (hy : y ∈ ball z W) :
(x, y) ∈ V.comp W
source
theorem UniformSpace.mem_comp_comp {β : Type ub} {V W M : SetRel β β} [W.IsSymm] {p : β × β} :
p ∈ (V.comp M).comp W ↔ (ball p.1 V ×ˢ ball p.2 W ∩ M).Nonempty

### Neighborhoods in uniform spaces #

source
theorem mem_nhds_uniformity_iff_right {α : Type ua} [UniformSpace α] {x : α} {s : Set α} :
s ∈ nhds x ↔ {p : α × α | p.1 = x → p.2 ∈ s} ∈ uniformity α
source
theorem mem_nhds_uniformity_iff_left {α : Type ua} [UniformSpace α] {x : α} {s : Set α} :
s ∈ nhds x ↔ {p : α × α | p.2 = x → p.1 ∈ s} ∈ uniformity α
source
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))
source
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))
source
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`.

source
theorem nhds_basis_uniformity' {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ι → Prop} {s : ι → SetRel α α} (h : (uniformity α).HasBasis p s) {x : α} :
(nhds x).HasBasis p fun (i : ι) => UniformSpace.ball x (s i)
source
theorem nhds_basis_uniformity {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ι → Prop} {s : ι → SetRel α α} (h : (uniformity α).HasBasis p s) {x : α} :
(nhds x).HasBasis p fun (i : ι) => {y : α | (y, x) ∈ s i}
source
theorem nhds_eq_comap_uniformity' {α : Type ua} [UniformSpace α] {x : α} :
nhds x = Filter.comap (fun (y : α) => (y, x)) (uniformity α)
source
theorem UniformSpace.mem_nhds_iff {α : Type ua} [UniformSpace α] {x : α} {s : Set α} :
s ∈ nhds x ↔ ∃ V ∈ uniformity α, ball x V ⊆ s
source
theorem UniformSpace.ball_mem_nhds {α : Type ua} [UniformSpace α] (x : α) ⦃V : SetRel α α⦄ (V_in : V ∈ uniformity α) :
ball x V ∈ nhds x
source
theorem UniformSpace.ball_mem_nhdsWithin {α : Type ua} [UniformSpace α] {x : α} {S : Set α} ⦃V : SetRel α α⦄ (x_in : x ∈ S) (V_in : V ∈ uniformity α ⊓ Filter.principal (S ×ˢ S)) :
ball x V ∈ nhdsWithin x S
source
theorem UniformSpace.mem_nhds_iff_symm {α : Type ua} [UniformSpace α] {x : α} {s : Set α} :
s ∈ nhds x ↔ ∃ V ∈ uniformity α, SetRel.IsSymm V ∧ ball x V ⊆ s
source
theorem UniformSpace.hasBasis_nhds {α : Type ua} [UniformSpace α] (x : α) :
(nhds x).HasBasis (fun (s : SetRel α α) => s ∈ uniformity α ∧ s.IsSymm) fun (s : SetRel α α) => ball x s
source
theorem UniformSpace.mem_closure_iff_symm_ball {α : Type ua} [UniformSpace α] {s : Set α} {x : α} :
x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ uniformity α → SetRel.IsSymm V → (s ∩ ball x V).Nonempty
source
theorem UniformSpace.mem_closure_iff_ball {α : Type ua} [UniformSpace α] {s : Set α} {x : α} :
x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ uniformity α → (ball x V ∩ s).Nonempty
source
theorem nhds_eq_uniformity {α : Type ua} [UniformSpace α] {x : α} :
nhds x = (uniformity α).lift' (UniformSpace.ball x)
source
theorem nhds_eq_uniformity' {α : Type ua} [UniformSpace α] {x : α} :
nhds x = (uniformity α).lift' fun (s : Set (α × α)) => {y : α | (y, x) ∈ s}
source
theorem mem_nhds_left {α : Type ua} [UniformSpace α] (x : α) {s : SetRel α α} (h : s ∈ uniformity α) :
{y : α | (x, y) ∈ s} ∈ nhds x
source
theorem mem_nhds_right {α : Type ua} [UniformSpace α] (y : α) {s : SetRel α α} (h : s ∈ uniformity α) :
{x : α | (x, y) ∈ s} ∈ nhds y
source
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
source
theorem tendsto_right_nhds_uniformity {α : Type ua} [UniformSpace α] {a : α} :
Filter.Tendsto (fun (a' : α) => (a', a)) (nhds a) (uniformity α)
source
theorem tendsto_left_nhds_uniformity {α : Type ua} [UniformSpace α] {a : α} :
Filter.Tendsto (fun (a' : α) => (a, a')) (nhds a) (uniformity α)
source
theorem lift_nhds_left {α : Type ua} {β : Type ub} [UniformSpace α] {x : α} {g : Set α → Filter β} (hg : Monotone g) :
(nhds x).lift g = (uniformity α).lift fun (s : SetRel α α) => g (UniformSpace.ball x s)
source
theorem lift_nhds_right {α : Type ua} {β : Type ub} [UniformSpace α] {x : α} {g : Set α → Filter β} (hg : Monotone g) :
(nhds x).lift g = (uniformity α).lift fun (s : SetRel α α) => g {y : α | (y, x) ∈ s}
source
theorem nhds_nhds_eq_uniformity_uniformity_prod {α : Type ua} [UniformSpace α] {a b : α} :
nhds a ×ˢ nhds b = (uniformity α).lift fun (s : SetRel α α) => (uniformity α).lift' fun (t : Set (α × α)) => {y : α | (y, a) ∈ s} ×ˢ {y : α | (b, y) ∈ t}
source
theorem Filter.HasBasis.biInter_biUnion_ball {α : Type ua} {ι : Sort u_1} [UniformSpace α] {p : ι → Prop} {U : ι → SetRel α α} (h : (uniformity α).HasBasis p U) (s : Set α) :
⋂ (i : ι), ⋂ (_ : p i), ⋃ x ∈ s, UniformSpace.ball x (U i) = closure s

### Uniform continuity #

source
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 β)

Instances For

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

Instances For

source
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 β)

Instances For

source
theorem uniformContinuous_def {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} :
UniformContinuous f ↔ ∀ r ∈ uniformity β, {x : α × α | (f x.1, f x.2) ∈ r} ∈ uniformity α
source
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
source
theorem uniformContinuousOn_univ {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {f : α → β} :
UniformContinuousOn f Set.univ ↔ UniformContinuous f
source
theorem uniformContinuous_of_const {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {c : α → β} (h : ∀ (a b : α), c a = c b) :
UniformContinuous c
source
theorem uniformContinuous_id {α : Type ua} [UniformSpace α] :
UniformContinuous id
source
theorem uniformContinuous_const {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {b : β} :
UniformContinuous fun (x : α) => b
source
theorem UniformContinuous.comp {α : Type ua} {β : Type ub} {γ : Type uc} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {g : β → γ} {f : α → β} (hg : UniformContinuous g) (hf : UniformContinuous f) :
UniformContinuous (g ∘ f)
source
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.

source
theorem Filter.HasBasis.uniformContinuous_iff {α : Type ua} {β : Type ub} {ι : Sort u_1} [UniformSpace α] {ι' : Sort u_2} [UniformSpace β] {p : ι → Prop} {s : ι → SetRel α α} (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
source
theorem Filter.HasBasis.uniformContinuousOn_iff {α : Type ua} {β : Type ub} {ι : Sort u_1} [UniformSpace α] {ι' : Sort u_2} [UniformSpace β] {p : ι → Prop} {s : ι → SetRel α α} (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