# mathlibdocumentation

topology.uniform_space.basic

# 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 `uniform_embedding.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 := (λ 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 `uniform_space.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: `is_open_iff_ball_subset {s : set X} : is_open 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 `id_rel = { 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 #

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

In this file we also define a complete lattice structure on the type `uniform_space X` of uniform structures on `X`, as well as the pullback (`uniform_space.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)`.

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

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

### Relations, seen as `set (α × α)`#

def id_rel {α : Type u_1} :
set × α)

The identity relation, or the graph of the identity function

Equations
@[simp]
theorem mem_id_rel {α : Type u_1} {a b : α} :
(a, b) id_rel a = b
@[simp]
theorem id_rel_subset {α : Type u_1} {s : set × α)} :
∀ (a : α), (a, a) s
def comp_rel {α : Type u} (r₁ r₂ : set × α)) :
set × α)

The composition of relations

Equations
@[simp]
theorem mem_comp_rel {α : Type u_1} {r₁ r₂ : set × α)} {x y : α} :
(x, y) comp_rel r₁ r₂ ∃ (z : α), (x, z) r₁ (z, y) r₂
@[simp]
theorem swap_id_rel {α : Type u_1} :
theorem monotone_comp_rel {α : Type u_1} {β : Type u_2} [preorder β] {f g : β → set × α)} (hf : monotone f) (hg : monotone g) :
monotone (λ (x : β), comp_rel (f x) (g x))
theorem comp_rel_mono {α : Type u_1} {f g h k : set × α)} (h₁ : f h) (h₂ : g k) :
g k
theorem prod_mk_mem_comp_rel {α : Type u_1} {a b c : α} {s t : set × α)} (h₁ : (a, c) s) (h₂ : (c, b) t) :
(a, b) t
@[simp]
theorem id_comp_rel {α : Type u_1} {r : set × α)} :
= r
theorem comp_rel_assoc {α : Type u_1} {r s t : set × α)} :
comp_rel (comp_rel r s) t = (comp_rel s t)
theorem left_subset_comp_rel {α : Type u_1} {s t : set × α)} (h : id_rel t) :
s t
theorem right_subset_comp_rel {α : Type u_1} {s t : set × α)} (h : id_rel s) :
t t
theorem subset_comp_self {α : Type u_1} {s : set × α)} (h : id_rel s) :
s s
theorem subset_iterate_comp_rel {α : Type u_1} {s t : set × α)} (h : id_rel s) (n : ) :
t ^[n] t
def symmetric_rel {α : Type u_1} (V : set × α)) :
Prop

The relation is invariant under swapping factors.

Equations
def symmetrize_rel {α : Type u_1} (V : set × α)) :
set × α)

The maximal symmetric relation contained in a given relation.

Equations
theorem symmetric_symmetrize_rel {α : Type u_1} (V : set × α)) :
theorem symmetrize_rel_subset_self {α : Type u_1} (V : set × α)) :
theorem symmetrize_mono {α : Type u_1} {V W : set × α)} (h : V W) :
theorem symmetric_rel.mk_mem_comm {α : Type u_1} {V : set × α)} (hV : symmetric_rel V) {x y : α} :
(x, y) V (y, x) V
theorem symmetric_rel_inter {α : Type u_1} {U V : set × α)} (hU : symmetric_rel U) (hV : symmetric_rel V) :
structure uniform_space.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.

Instances for `uniform_space.core`
def uniform_space.core.mk' {α : Type u} (U : filter × α)) (refl : ∀ (r : set × α)), r U∀ (x : α), (x, x) r) (symm : ∀ (r : set × α)), r U U) (comp : ∀ (r : set × α)), r U(∃ (t : set × α)) (H : t U), t r)) :

An alternative constructor for `uniform_space.core`. This version unfolds various `filter`-related definitions.

Equations
def uniform_space.core.mk_of_basis {α : Type u} (B : filter_basis × α)) (refl : ∀ (r : set × α)), r B∀ (x : α), (x, x) r) (symm : ∀ (r : set × α)), r B(∃ (t : set × α)) (H : t B), t ) (comp : ∀ (r : set × α)), r B(∃ (t : set × α)) (H : t B), t r)) :

Defining an `uniform_space.core` from a filter basis satisfying some uniformity-like axioms.

Equations

A uniform space generates a topological space

Equations
theorem uniform_space.core_eq {α : Type u_1} {u₁ u₂ : uniform_space.core α} :
u₁.uniformity = u₂.uniformityu₁ = u₂
@[class]
structure uniform_space (α : Type u) :
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.

Instances of this typeclass
Instances of other typeclasses for `uniform_space`
def uniform_space.mk' {α : Type u_1} (t : topological_space α) (c : uniform_space.core α) (is_open_uniformity : ∀ (s : set α), t.is_open s ∀ (x : α), x s{p : α × α | p.fst = xp.snd s} c.uniformity) :

Alternative constructor for `uniform_space α` when a topology is already given.

Equations
def uniform_space.of_core {α : Type u} (u : uniform_space.core α) :

Construct a `uniform_space` from a `uniform_space.core`.

Equations
def uniform_space.of_core_eq {α : Type u} (u : uniform_space.core α) (t : topological_space α) (h : t = u.to_topological_space) :

Construct a `uniform_space` from a `u : uniform_space.core` and a `topological_space` structure that is equal to `u.to_topological_space`.

Equations
@[ext]
theorem uniform_space_eq {α : Type u_1} {u₁ u₂ : uniform_space α} :
theorem uniform_space.of_core_eq_to_core {α : Type u_1} (u : uniform_space α) (t : topological_space α)  :
def uniform_space.replace_topology {α : Type u_1} [i : topological_space α] (u : uniform_space α)  :

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

Equations
theorem uniform_space.replace_topology_eq {α : Type u_1} [i : topological_space α] (u : uniform_space α)  :
= u
def uniformity (α : Type u)  :
filter × α)

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

Equations
Instances for `uniformity`
theorem is_open_uniformity {α : Type u_1} {s : set α} :
∀ (x : α), x s{p : α × α | p.fst = xp.snd s}
theorem refl_le_uniformity {α : Type u_1}  :
@[protected, instance]
def uniformity.ne_bot {α : Type u_1} [nonempty α] :
theorem refl_mem_uniformity {α : Type u_1} {x : α} {s : set × α)} (h : s ) :
(x, x) s
theorem mem_uniformity_of_eq {α : Type u_1} {x y : α} {s : set × α)} (h : s ) (hx : x = y) :
(x, y) s
theorem symm_le_uniformity {α : Type u_1}  :
theorem comp_le_uniformity {α : Type u_1}  :
(uniformity α).lift' (λ (s : set × α)), s)
theorem tendsto_swap_uniformity {α : Type u_1}  :
theorem comp_mem_uniformity_sets {α : Type u_1} {s : set × α)} (hs : s ) :
∃ (t : set × α)) (H : t , t s
theorem eventually_uniformity_iterate_comp_subset {α : Type u_1} {s : set × α)} (hs : s ) (n : ) :
∀ᶠ (t : set × α)) in (uniformity α).small_sets, ^[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 u_1} {s : set × α)} (hs : s ) :
∀ᶠ (t : set × α)) in (uniformity α).small_sets, t s

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

theorem filter.tendsto.uniformity_trans {α : Type u_1} {β : Type u_2} {l : filter β} {f₁ f₂ f₃ : β → α} (h₁₂ : filter.tendsto (λ (x : β), (f₁ x, f₂ x)) l (uniformity α)) (h₂₃ : filter.tendsto (λ (x : β), (f₂ x, f₃ x)) l (uniformity α)) :
filter.tendsto (λ (x : β), (f₁ x, f₃ x)) l (uniformity α)

Relation `λ f g, tendsto (λ x, (f x, g x)) l (𝓤 α)` is transitive.

theorem filter.tendsto.uniformity_symm {α : Type u_1} {β : Type u_2} {l : filter β} {f : β → α × α} (h : (uniformity α)) :
filter.tendsto (λ (x : β), ((f x).snd, (f x).fst)) l (uniformity α)

Relation `λ f g, tendsto (λ x, (f x, g x)) l (𝓤 α)` is symmetric

theorem tendsto_diag_uniformity {α : Type u_1} {β : Type u_2} (f : β → α) (l : filter β) :
filter.tendsto (λ (x : β), (f x, f x)) l (uniformity α)

Relation `λ f g, tendsto (λ x, (f x, g x)) l (𝓤 α)` is reflexive.

theorem tendsto_const_uniformity {α : Type u_1} {β : Type u_2} {a : α} {f : filter β} :
filter.tendsto (λ (_x : β), (a, a)) f (uniformity α)
theorem symm_of_uniformity {α : Type u_1} {s : set × α)} (hs : s ) :
∃ (t : set × α)) (H : t , (∀ (a b : α), (a, b) t(b, a) t) t s
theorem comp_symm_of_uniformity {α : Type u_1} {s : set × α)} (hs : s ) :
∃ (t : set × α)) (H : t , (∀ {a b : α}, (a, b) t(b, a) t) t s
theorem uniformity_le_symm {α : Type u_1}  :
theorem uniformity_eq_symm {α : Type u_1}  :
@[simp]
theorem comap_swap_uniformity {α : Type u_1}  :
theorem symmetrize_mem_uniformity {α : Type u_1} {V : set × α)} (h : V ) :
theorem uniformity_lift_le_swap {α : Type u_1} {β : Type u_2} {g : set × α)} {f : filter β} (hg : monotone g) (h : (uniformity α).lift (λ (s : set × α)), g (prod.swap ⁻¹' s)) f) :
theorem uniformity_lift_le_comp {α : Type u_1} {β : Type u_2} {f : set × α)} (h : monotone f) :
(uniformity α).lift (λ (s : set × α)), f (comp_rel s s)) (uniformity α).lift f
theorem comp_le_uniformity3 {α : Type u_1}  :
(uniformity α).lift' (λ (s : set × α)), (comp_rel s s))
theorem comp_symm_mem_uniformity_sets {α : Type u_1} {s : set × α)} (hs : s ) :
∃ (t : set × α)) (H : t , t s

See also `comp_open_symm_mem_uniformity_sets`.

theorem subset_comp_self_of_mem_uniformity {α : Type u_1} {s : set × α)} (h : s ) :
s s
theorem comp_comp_symm_mem_uniformity_sets {α : Type u_1} {s : set × α)} (hs : s ) :
∃ (t : set × α)) (H : t , comp_rel (comp_rel t t) t s

### Balls in uniform spaces #

def uniform_space.ball {β : Type u_2} (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
theorem uniform_space.mem_ball_self {α : Type u_1} (x : α) {V : set × α)} (hV : V ) :
x
theorem mem_ball_comp {β : Type u_2} {V W : set × β)} {x y z : β} (h : y ) (h' : z ) :
z (comp_rel V W)

The triangle inequality for `uniform_space.ball`

theorem ball_subset_of_comp_subset {β : Type u_2} {V W : set × β)} {x y : β} (h : x ) (h' : W V) :
theorem ball_mono {β : Type u_2} {V W : set × β)} (h : V W) (x : β) :
theorem ball_inter {β : Type u_2} (x : β) (V W : set × β)) :
(V W) =
theorem ball_inter_left {β : Type u_2} (x : β) (V W : set × β)) :
(V W)
theorem ball_inter_right {β : Type u_2} (x : β) (V W : set × β)) :
(V W)
theorem mem_ball_symmetry {β : Type u_2} {V : set × β)} (hV : symmetric_rel V) {x y : β} :
x y
theorem ball_eq_of_symmetry {β : Type u_2} {V : set × β)} (hV : symmetric_rel V) {x : β} :
= {y : β | (y, x) V}
theorem mem_comp_of_mem_ball {β : Type u_2} {V W : set × β)} {x y z : β} (hV : symmetric_rel V) (hx : x ) (hy : y ) :
(x, y) W
theorem uniform_space.is_open_ball {α : Type u_1} (x : α) {V : set × α)} (hV : is_open V) :
theorem mem_comp_comp {β : Type u_2} {V W M : set × β)} (hW' : symmetric_rel W) {p : β × β} :

### Neighborhoods in uniform spaces #

theorem mem_nhds_uniformity_iff_right {α : Type u_1} {x : α} {s : set α} :
s nhds x {p : α × α | p.fst = xp.snd s}
theorem mem_nhds_uniformity_iff_left {α : Type u_1} {x : α} {s : set α} :
s nhds x {p : α × α | p.snd = xp.fst s}
theorem nhds_eq_comap_uniformity_aux {α : Type u} {x : α} {s : set α} {F : filter × α)} :
{p : α × α | p.fst = xp.snd s} F s F
theorem nhds_eq_comap_uniformity {α : Type u_1} {x : α} :
theorem is_open_iff_ball_subset {α : Type u_1} {s : set α} :
∀ (x : α), x s(∃ (V : set × α)) (H : V , s)

See also `is_open_iff_open_ball_subset`.

theorem nhds_basis_uniformity' {α : Type u_1} {ι : Sort u_5} {p : ι → Prop} {s : ι → set × α)} (h : (uniformity α).has_basis p s) {x : α} :
(nhds x).has_basis p (λ (i : ι), (s i))
theorem nhds_basis_uniformity {α : Type u_1} {ι : Sort u_5} {p : ι → Prop} {s : ι → set × α)} (h : (uniformity α).has_basis p s) {x : α} :
(nhds x).has_basis p (λ (i : ι), {y : α | (y, x) s i})
theorem uniform_space.mem_nhds_iff {α : Type u_1} {x : α} {s : set α} :
s nhds x ∃ (V : set × α)) (H : V , s
theorem uniform_space.ball_mem_nhds {α : Type u_1} (x : α) ⦃V : set × α) (V_in : V ) :
theorem uniform_space.mem_nhds_iff_symm {α : Type u_1} {x : α} {s : set α} :
s nhds x ∃ (V : set × α)) (H : V , s
theorem uniform_space.has_basis_nhds {α : Type u_1} (x : α) :
(nhds x).has_basis (λ (s : set × α)), s (λ (s : set × α)),
theorem uniform_space.mem_closure_iff_symm_ball {α : Type u_1} {s : set α} {x : α} :
x ∀ {V : set × α)}, V (s .nonempty
theorem uniform_space.mem_closure_iff_ball {α : Type u_1} {s : set α} {x : α} :
x ∀ {V : set × α)}, V s).nonempty
theorem uniform_space.has_basis_nhds_prod {α : Type u_1} (x y : α) :
(nhds (x, y)).has_basis (λ (s : set × α)), s (λ (s : set × α)),
theorem nhds_eq_uniformity {α : Type u_1} {x : α} :
theorem mem_nhds_left {α : Type u_1} (x : α) {s : set × α)} (h : s ) :
{y : α | (x, y) s} nhds x
theorem mem_nhds_right {α : Type u_1} (y : α) {s : set × α)} (h : s ) :
{x : α | (x, y) s} nhds y
theorem tendsto_right_nhds_uniformity {α : Type u_1} {a : α} :
filter.tendsto (λ (a' : α), (a', a)) (nhds a) (uniformity α)
theorem tendsto_left_nhds_uniformity {α : Type u_1} {a : α} :
filter.tendsto (λ (a' : α), (a, a')) (nhds a) (uniformity α)
theorem lift_nhds_left {α : Type u_1} {β : Type u_2} {x : α} {g : set α} (hg : monotone g) :
(nhds x).lift g = (uniformity α).lift (λ (s : set × α)), g {y : α | (x, y) s})
theorem lift_nhds_right {α : Type u_1} {β : Type u_2} {x : α} {g : set α} (hg : monotone g) :
(nhds x).lift g = (uniformity α).lift (λ (s : set × α)), g {y : α | (y, x) s})
theorem nhds_nhds_eq_uniformity_uniformity_prod {α : Type u_1} {a b : α} :
(nhds a).prod (nhds b) = (uniformity α).lift (λ (s : set × α)), (uniformity α).lift' (λ (t : set × α)), {y : α | (y, a) s} ×ˢ {y : α | (b, y) t}))
theorem nhds_eq_uniformity_prod {α : Type u_1} {a b : α} :
nhds (a, b) = (uniformity α).lift' (λ (s : set × α)), {y : α | (y, a) s} ×ˢ {y : α | (b, y) s})
theorem nhdset_of_mem_uniformity {α : Type u_1} {d : set × α)} (s : set × α)) (hd : d ) :
∃ (t : set × α)), s t t {p : α × α | ∃ (x y : α), (p.fst, x) d (x, y) s (y, p.snd) d}
theorem nhds_le_uniformity {α : Type u_1} (x : α) :
nhds (x, x)

Entourages are neighborhoods of the diagonal.

theorem supr_nhds_le_uniformity {α : Type u_1}  :
(⨆ (x : α), nhds (x, x))

Entourages are neighborhoods of the diagonal.

### Closure and interior in uniform spaces #

theorem closure_eq_uniformity {α : Type u_1} (s : set × α)) :
= ⋂ (V : set × α)) (H : V {V : set × α) | V , comp_rel (comp_rel V s) V
theorem uniformity_has_basis_closed {α : Type u_1}  :
(uniformity α).has_basis (λ (V : set × α)), V id
theorem uniformity_has_basis_closure {α : Type u_1}  :
(uniformity α).has_basis (λ (V : set × α)), V closure

Closed entourages form a basis of the uniformity filter.

theorem closure_eq_inter_uniformity {α : Type u_1} {t : set × α)} :
= ⋂ (d : set × α)) (H : d , (comp_rel t d)
theorem uniformity_eq_uniformity_closure {α : Type u_1}  :
theorem uniformity_eq_uniformity_interior {α : Type u_1}  :
theorem interior_mem_uniformity {α : Type u_1} {s : set × α)} (hs : s ) :
theorem mem_uniformity_is_closed {α : Type u_1} {s : set × α)} (h : s ) :
∃ (t : set × α)) (H : t , t s
theorem is_open_iff_open_ball_subset {α : Type u_1} {s : set α} :
∀ (x : α), x s(∃ (V : set × α)) (H : V , s)
theorem dense.bUnion_uniformity_ball {α : Type u_1} {s : set α} {U : set × α)} (hs : dense s) (hU : U ) :
(⋃ (x : α) (H : x s), = set.univ

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

### Uniformity bases #

theorem uniformity_has_basis_open {α : Type u_1}  :
(uniformity α).has_basis (λ (V : set × α)), V is_open V) id

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

theorem filter.has_basis.mem_uniformity_iff {α : Type u_1} {β : Type u_2} {p : β → Prop} {s : β → set × α)} (h : (uniformity α).has_basis p s) {t : set × α)} :
t ∃ (i : β) (hi : p i), ∀ (a b : α), (a, b) s i(a, b) t
theorem uniform_space.has_basis_symmetric {α : Type u_1}  :
(uniformity α).has_basis (λ (s : set × α)), s id

Symmetric entourages form a basis of `𝓤 α`

theorem uniformity_has_basis_open_symmetric {α : Type u_1}  :
(uniformity α).has_basis (λ (V : set × α)), 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 u_1} {s : set × α)} (hs : s ) :
∃ (t : set × α)) (H : t , t s
theorem uniform_space.has_seq_basis (α : Type u_1)  :
∃ (V : set × α)), ∀ (n : ), symmetric_rel (V n)
theorem filter.has_basis.bInter_bUnion_ball {α : Type u_1} {ι : Sort u_5} {p : ι → Prop} {U : ι → set × α)} (h : (uniformity α).has_basis p U) (s : set α) :
(⋂ (i : ι) (hi : p i), ⋃ (x : α) (H : x s), (U i)) =

### Uniform continuity #

def uniform_continuous {α : Type u_1} {β : Type u_2} (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
Instances for `uniform_continuous`
def uniform_continuous_on {α : Type u_1} {β : Type u_2} (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
theorem uniform_continuous_def {α : Type u_1} {β : Type u_2} {f : α → β} :
∀ (r : set × β)), r {x : α × α | (f x.fst, f x.snd) r}
theorem uniform_continuous_iff_eventually {α : Type u_1} {β : Type u_2} {f : α → β} :
∀ (r : set × β)), r (∀ᶠ (x : α × α) in , (f x.fst, f x.snd) r)
theorem uniform_continuous_on_univ {α : Type u_1} {β : Type u_2} {f : α → β} :
theorem uniform_continuous_of_const {α : Type u_1} {β : Type u_2} {c : α → β} (h : ∀ (a b : α), c a = c b) :
theorem uniform_continuous_id {α : Type u_1}  :
theorem uniform_continuous_const {α : Type u_1} {β : Type u_2} {b : β} :
uniform_continuous (λ (a : α), b)
theorem uniform_continuous.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β} (hg : uniform_continuous g) (hf : uniform_continuous f) :
theorem filter.has_basis.uniform_continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {p : γ → Prop} {s : γ → set × α)} (ha : (uniformity α).has_basis p s) {q : δ → Prop} {t : δ → set × β)} (hb : (uniformity β).has_basis q t) {f : α → β} :
∀ (i : δ), q i(∃ (j : γ) (hj : p j), ∀ (x y : α), (x, y) s j(f x, f y) t i)
theorem filter.has_basis.uniform_continuous_on_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {p : γ → Prop} {s : γ → set × α)} (ha : (uniformity α).has_basis p s) {q : δ → Prop} {t : δ → set × β)} (hb : (uniformity β).has_basis q t) {f : α → β} {S : set α} :
∀ (i : δ), q i(∃ (j : γ) (hj : p j), ∀ (x : α), x S∀ (y : α), y S(x, y) s j(f x, f y) t i)
@[protected, instance]
def uniform_space.partial_order {α : Type u_1} :
Equations
@[protected, instance]
def uniform_space.has_Inf {α : Type u_1} :
Equations
@[protected, instance]
def uniform_space.has_top {α : Type u_1} :
Equations
@[protected, instance]
def uniform_space.has_bot {α : Type u_1} :
Equations
@[protected, instance]
def uniform_space.has_inf {α : Type u_1} :
Equations
@[protected, instance]
def uniform_space.complete_lattice {α : Type u_1} :
Equations
theorem infi_uniformity {α : Type u_1} {ι : Sort u_2} {u : ι → } :
theorem infi_uniformity' {α : Type u_1} {ι : Sort u_2} {u : ι → } :
= ⨅ (i : ι),
theorem inf_uniformity {α : Type u_1} {u v : uniform_space α} :
theorem inf_uniformity' {α : Type u_1} {u v : uniform_space α} :
=
@[protected, instance]
def inhabited_uniform_space {α : Type u_1} :
Equations
@[protected, instance]
def inhabited_uniform_space_core {α : Type u_1} :
Equations
def uniform_space.comap {α : Type u_1} {β : Type u_2} (f : α → β) (u : uniform_space β) :

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 `α × α → β × β`.

Equations
theorem uniformity_comap {α : Type u_1} {β : Type u_2} {f : α → β} (h : _inst_1 = _inst_2) :
theorem uniform_space_comap_id {α : Type u_1} :
theorem uniform_space.comap_comap {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uγ : uniform_space γ] {f : α → β} {g : β → γ} :
theorem uniform_space.comap_inf {α : Type u_1} {γ : Type u_2} {u₁ u₂ : uniform_space γ} {f : α → γ} :
(u₁ u₂) =
theorem uniform_space.comap_infi {ι : Sort u_1} {α : Type u_2} {γ : Type u_3} {u : ι → } {f : α → γ} :
(⨅ (i : ι), u i) = ⨅ (i : ι), (u i)
theorem uniform_space.comap_mono {α : Type u_1} {γ : Type u_2} {f : α → γ} :
monotone (λ (u : ,
theorem uniform_continuous_iff {α : Type u_1} {β : Type u_2} [uα : uniform_space α] [uβ : uniform_space β] {f : α → β} :
theorem le_iff_uniform_continuous_id {α : Type u_1} {u v : uniform_space α} :
theorem uniform_continuous_comap {α : Type u_1} {β : Type u_2} {f : α → β} [u : uniform_space β] :
theorem to_topological_space_comap {α : Type u_1} {β : Type u_2} {f : α → β} {u : uniform_space β} :
theorem uniform_continuous_comap' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : γ → β} {g : α → γ} [v : uniform_space β] [u : uniform_space α] (h : uniform_continuous (f g)) :
theorem to_nhds_mono {α : Type u_1} {u₁ u₂ : uniform_space α} (h : u₁ u₂) (a : α) :
theorem to_topological_space_mono {α : Type u_1} {u₁ u₂ : uniform_space α} (h : u₁ u₂) :
theorem uniform_continuous.continuous {α : Type u_1} {β : Type u_2} {f : α → β} (hf : uniform_continuous f) :
theorem to_topological_space_bot {α : Type u_1} :
theorem to_topological_space_top {α : Type u_1} :
theorem to_topological_space_infi {α : Type u_1} {ι : Sort u_2} {u : ι → } :
theorem to_topological_space_inf {α : Type u_1} {u v : uniform_space α} :
theorem discrete_topology_of_discrete_uniformity {α : Type u_1} [hα : uniform_space α]  :

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

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def subtype.uniform_space {α : Type u_1} {p : α → Prop} [t : uniform_space α] :
Equations
theorem uniformity_subtype {α : Type u_1} {p : α → Prop} [t : uniform_space α] :
= filter.comap (λ (q : × subtype p), (q.fst.val, q.snd.val)) (uniformity α)
theorem uniform_continuous_subtype_val {α : Type u_1} {p : α → Prop}  :
theorem uniform_continuous_subtype_coe {α : Type u_1} {p : α → Prop}  :
theorem uniform_continuous_subtype_mk {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : β → α} (hf : uniform_continuous f) (h : ∀ (x : β), p (f x)) :
uniform_continuous (λ (x : β), f x, _⟩)
theorem uniform_continuous_on_iff_restrict {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} :
theorem tendsto_of_uniform_continuous_subtype {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {a : α} (hf : uniform_continuous (λ (x : s), f x.val)) (ha : s nhds a) :
(nhds a) (nhds (f a))
theorem uniform_continuous_on.continuous_on {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} (h : s) :
@[protected, instance]
def add_opposite.uniform_space {α : Type u_1}  :
Equations
@[protected, instance]
def mul_opposite.uniform_space {α : Type u_1}  :
Equations
theorem uniformity_mul_opposite {α : Type u_1}  :
theorem uniformity_add_opposite {α : Type u_1}  :
@[simp]
theorem comap_uniformity_mul_opposite {α : Type u_1}  :
filter.comap (λ (p : α × α), , =
@[simp]
theorem comap_uniformity_add_opposite {α : Type u_1}  :
filter.comap (λ (p : α × α), , =
theorem mul_opposite.uniform_continuous_unop {α : Type u_1}  :
theorem add_opposite.uniform_continuous_unop {α : Type u_1}  :
theorem add_opposite.uniform_continuous_op {α : Type u_1}  :
theorem mul_opposite.uniform_continuous_op {α : Type u_1}  :
@[protected, instance]
def prod.uniform_space {α : Type u_1} {β : Type u_2} [u₁ : uniform_space α] [u₂ : uniform_space β] :
Equations
theorem uniformity_prod {α : Type u_1} {β : Type u_2}  :
uniformity × β) = filter.comap (λ (p : × β) × α × β), (p.fst.fst, p.snd.fst)) (uniformity α) filter.comap (λ (p : × β) × α × β), (p.fst.snd, p.snd.snd)) (uniformity β)
theorem uniformity_prod_eq_prod {α : Type u_1} {β : Type u_2}  :
uniformity × β) = filter.map (λ (p : × α) × β × β), ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ((uniformity α).prod (uniformity β))
theorem mem_map_iff_exists_image' {α : Type u_1} {β : Type u_2} {f : filter α} {m : α → β} {t : set β} :
t f).sets ∃ (s : set α) (H : s f), m '' s t
theorem mem_uniformity_of_uniform_continuous_invariant {α : Type u_1} {s : set × α)} {f : α → α → α} (hf : uniform_continuous (λ (p : α × α), f p.fst p.snd)) (hs : s ) :
∃ (u : set × α)) (H : u , ∀ (a b c : α), (a, b) u(f a c, f b c) s
theorem mem_uniform_prod {α : Type u_1} {β : Type u_2} [t₁ : uniform_space α] [t₂ : uniform_space β] {a : set × α)} {b : set × β)} (ha : a ) (hb : b ) :
{p : × β) × α × β | (p.fst.fst, p.snd.fst) a (p.fst.snd, p.snd.snd) b} uniformity × β)
theorem tendsto_prod_uniformity_fst {α : Type u_1} {β : Type u_2}  :
filter.tendsto (λ (p : × β) × α × β), (p.fst.fst, p.snd.fst)) (uniformity × β)) (uniformity α)
theorem tendsto_prod_uniformity_snd {α : Type u_1} {β : Type u_2}  :
filter.tendsto (λ (p : × β) × α × β), (p.fst.snd, p.snd.snd)) (uniformity × β)) (uniformity β)
theorem uniform_continuous_fst {α : Type u_1} {β : Type u_2}  :
uniform_continuous (λ (p : α × β), p.fst)
theorem uniform_continuous_snd {α : Type u_1} {β : Type u_2}  :
uniform_continuous (λ (p : α × β), p.snd)
theorem uniform_continuous.prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f₁ : α → β} {f₂ : α → γ} (h₁ : uniform_continuous f₁) (h₂ : uniform_continuous f₂) :
uniform_continuous (λ (a : α), (f₁ a, f₂ a))
theorem uniform_continuous.prod_mk_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × β → γ} (h : uniform_continuous f) (b : β) :
uniform_continuous (λ (a : α), f (a, b))
theorem uniform_continuous.prod_mk_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × β → γ} (h : uniform_continuous f) (a : α) :
uniform_continuous (λ (b : β), f (a, b))
theorem uniform_continuous.prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} (hf : uniform_continuous f) (hg : uniform_continuous g) :
theorem to_topological_space_prod {α : Type u_1} {β : Type u_2} [u : uniform_space α] [v : uniform_space β] :
def uniform_continuous₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) :
Prop

Uniform continuity for functions of two variables.

Equations
theorem uniform_continuous₂_def {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) :
theorem uniform_continuous₂.uniform_continuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} (h : uniform_continuous₂ f) :
theorem uniform_continuous₂_curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α × β → γ) :
theorem uniform_continuous₂.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β → γ} {g : γ → δ} (hg : uniform_continuous g) (hf : uniform_continuous₂ f) :
theorem uniform_continuous₂.bicompl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {δ' : Type u_6} [uniform_space δ'] {f : α → β → γ} {ga : δ → α} {gb : δ' → β} (hf : uniform_continuous₂ f) (hga : uniform_continuous ga) (hgb : uniform_continuous gb) :
theorem to_topological_space_subtype {α : Type u_1} [u : uniform_space α] {p : α → Prop} :
def uniform_space.core.sum {α : Type u_1} {β : Type u_2}  :

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
theorem union_mem_uniformity_sum {α : Type u_1} {β : Type u_2} {a : set × α)} (ha : a ) {b : set × β)} (hb : b ) :
(λ (p : α × α), (sum.inl p.fst, sum.inl p.snd)) '' a (λ (p : β × β), (sum.inr p.fst, sum.inr p.snd)) '' b uniform_space.core.sum.uniformity

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

theorem uniformity_sum_of_open_aux {α : Type u_1} {β : Type u_2} {s : set β)} (hs : is_open s) {x : α β} (xs : x s) :
{p : β) × β) | p.fst = xp.snd s} uniform_space.core.sum.uniformity
theorem open_of_uniformity_sum_aux {α : Type u_1} {β : Type u_2} {s : set β)} (hs : ∀ (x : α β), x s{p : β) × β) | p.fst = xp.snd s} uniform_space.core.sum.uniformity) :
@[protected, instance]
def sum.uniform_space {α : Type u_1} {β : Type u_2}  :
Equations
theorem sum.uniformity {α : Type u_1} {β : Type u_2}  :
uniformity β) = filter.map (λ (p : α × α), (sum.inl p.fst, sum.inl p.snd)) (uniformity α) filter.map (λ (p : β × β), (sum.inr p.fst, sum.inr p.snd)) (uniformity β)
theorem lebesgue_number_lemma {α : Type u} {s : set α} {ι : Sort u_1} {c : ι → set α} (hs : is_compact s) (hc₁ : ∀ (i : ι), is_open (c i)) (hc₂ : s ⋃ (i : ι), c i) :
∃ (n : set × α)) (H : n , ∀ (x : α), x s(∃ (i : ι), {y : α | (x, y) n} c i)

Let `c : ι → set α` be an open cover of a compact set `s`. Then there exists an entourage `n` such that for each `x ∈ s` its `n`-neighborhood is contained in some `c i`.

theorem lebesgue_number_lemma_sUnion {α : Type u} {s : set α} {c : set (set α)} (hs : is_compact s) (hc₁ : ∀ (t : set α), t c) (hc₂ : s ⋃₀ c) :
∃ (n : set × α)) (H : n , ∀ (x : α), x s(∃ (t : set α) (H : t c), ∀ (y : α), (x, y) ny t)

Let `c : set (set α)` be an open cover of a compact set `s`. Then there exists an entourage `n` such that for each `x ∈ s` its `n`-neighborhood is contained in some `t ∈ c`.

theorem lebesgue_number_of_compact_open {α : Type u_1} {K U : set α} (hK : is_compact K) (hU : is_open U) (hKU : K U) :
∃ (V : set × α)) (H : V , ∀ (x : α), x K U

A useful consequence of the Lebesgue number lemma: given any compact set `K` contained in an open set `U`, we can find an (open) entourage `V` such that the ball of size `V` about any point of `K` is contained in `U`.

### 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 u_1} {β : Type u_2} {f : filter β} {u : β → α} {a : α} :
(nhds a) filter.tendsto (λ (x : β), (a, u x)) f (uniformity α)
theorem uniform.tendsto_nhds_left {α : Type u_1} {β : Type u_2} {f : filter β} {u : β → α} {a : α} :
(nhds a) filter.tendsto (λ (x : β), (u x, a)) f (uniformity α)
theorem uniform.continuous_at_iff'_right {α : Type u_1} {β : Type u_2} {f : β → α} {b : β} :
filter.tendsto (λ (x : β), (f b, f x)) (nhds b) (uniformity α)
theorem uniform.continuous_at_iff'_left {α : Type u_1} {β : Type u_2} {f : β → α} {b : β} :
filter.tendsto (λ (x : β), (f x, f b)) (nhds b) (uniformity α)
theorem uniform.continuous_at_iff_prod {α : Type u_1} {β : Type u_2} {f : β → α} {b : β} :
filter.tendsto (λ (x : β × β), (f x.fst, f x.snd)) (nhds (b, b)) (uniformity α)
theorem uniform.continuous_within_at_iff'_right {α : Type u_1} {β : Type u_2} {f : β → α} {b : β} {s : set β} :
b filter.tendsto (λ (x : β), (f b, f x)) s) (uniformity α)
theorem uniform.continuous_within_at_iff'_left {α : Type u_1} {β : Type u_2} {f : β → α} {b : β} {s : set β} :
b filter.tendsto (λ (x : β), (f x, f b)) s) (uniformity α)
theorem uniform.continuous_on_iff'_right {α : Type u_1} {β : Type u_2} {f : β → α} {s : set β} :
∀ (b : β), b sfilter.tendsto (λ (x : β), (f b, f x)) s) (uniformity α)
theorem uniform.continuous_on_iff'_left {α : Type u_1} {β : Type u_2} {f : β → α} {s : set β} :
∀ (b : β), b sfilter.tendsto (λ (x : β), (f x, f b)) s) (uniformity α)
theorem uniform.continuous_iff'_right {α : Type u_1} {β : Type u_2} {f : β → α} :
∀ (b : β), filter.tendsto (λ (x : β), (f b, f x)) (nhds b) (uniformity α)
theorem uniform.continuous_iff'_left {α : Type u_1} {β : Type u_2} {f : β → α} :
∀ (b : β), filter.tendsto (λ (x : β), (f x, f b)) (nhds b) (uniformity α)
theorem filter.tendsto.congr_uniformity {α : Type u_1} {β : Type u_2} {f g : α → β} {l : filter α} {b : β} (hf : (nhds b)) (hg : filter.tendsto (λ (x : α), (f x, g x)) l (uniformity β)) :
(nhds b)
theorem uniform.tendsto_congr {α : Type u_1} {β : Type u_2} {f g : α → β} {l : filter α} {b : β} (hfg : filter.tendsto (λ (x : α), (f x, g x)) l (uniformity β)) :
(nhds b) (nhds b)