mathlib documentation

topology.​uniform_space.​basic

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.

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:

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:

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:

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

 Main definitions

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 × α)} :
id_rel s ∀ (a : α), (a, a) s

def comp_rel {α : Type u} :
set × α)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 × α)} :
monotone fmonotone gmonotone (λ (x : β), comp_rel (f x) (g x))

theorem comp_rel_mono {α : Type u_1} {f g h k : set × α)} :
f hg kcomp_rel f g comp_rel h k

theorem prod_mk_mem_comp_rel {α : Type u_1} {a b c : α} {s t : set × α)} :
(a, c) s(c, b) t(a, b) comp_rel s t

@[simp]
theorem id_comp_rel {α : Type u_1} {r : set × α)} :

theorem comp_rel_assoc {α : Type u_1} {r s t : set × α)} :

theorem subset_comp_self {α : Type u_1} {s : set × α)} :
id_rel ss comp_rel s s

def symmetric_rel {α : Type u_1} :
set × α) → Prop

The relation is invariant under swapping factors.

Equations
def symmetrize_rel {α : Type u_1} :
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 × α)} :

theorem symmetric_rel_inter {α : Type u_1} {U V : set × α)} :

structure uniform_space.​core  :
Type uType 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.

def uniform_space.​core.​mk' {α : Type u} (U : filter × α)) :
(∀ (r : set × α)), r U∀ (x : α), (x, x) r)(∀ (r : set × α)), r Uprod.swap ⁻¹' r U)(∀ (r : set × α)), r U(∃ (t : set × α)) (H : t U), comp_rel t t r))uniform_space.core α

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

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 uType 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
def uniform_space.​mk' {α : Type u_1} (t : topological_space α) (c : uniform_space.core α) :
(∀ (s : set α), t.is_open s ∀ (x : α), x s{p : α × α | p.fst = xp.snd s} c.uniformity)uniform_space α

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

Equations

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 α} :

def uniformity (α : Type u) [uniform_space α] :
filter × α)

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

Equations
theorem is_open_uniformity {α : Type u_1} [uniform_space α] {s : set α} :
is_open s ∀ (x : α), x s{p : α × α | p.fst = xp.snd s} uniformity α

theorem refl_mem_uniformity {α : Type u_1} [uniform_space α] {x : α} {s : set × α)} :
s uniformity α(x, x) s

theorem comp_le_uniformity {α : Type u_1} [uniform_space α] :
(uniformity α).lift' (λ (s : set × α)), comp_rel s s) uniformity α

theorem comp_mem_uniformity_sets {α : Type u_1} [uniform_space α] {s : set × α)} :
s uniformity α(∃ (t : set × α)) (H : t uniformity α), comp_rel t t s)

theorem filter.​tendsto.​uniformity_trans {α : Type u_1} {β : Type u_2} [uniform_space α] {l : filter β} {f₁ f₂ f₃ : β → α} :
filter.tendsto (λ (x : β), (f₁ x, f₂ x)) l (uniformity α)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} [uniform_space α] {l : filter β} {f : β → α × α} :
filter.tendsto f l (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} [uniform_space α] (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} [uniform_space α] {a : α} {f : filter β} :
filter.tendsto (λ (_x : β), (a, a)) f (uniformity α)

theorem symm_of_uniformity {α : Type u_1} [uniform_space α] {s : set × α)} :
s uniformity α(∃ (t : set × α)) (H : t uniformity α), (∀ (a b : α), (a, b) t(b, a) t) t s)

theorem comp_symm_of_uniformity {α : Type u_1} [uniform_space α] {s : set × α)} :
s uniformity α(∃ (t : set × α)) (H : t uniformity α), (∀ {a b : α}, (a, b) t(b, a) t) comp_rel t t s)

theorem uniformity_eq_symm {α : Type u_1} [uniform_space α] :

theorem symmetrize_mem_uniformity {α : Type u_1} [uniform_space α] {V : set × α)} :

theorem uniformity_lift_le_swap {α : Type u_1} {β : Type u_2} [uniform_space α] {g : set × α)filter β} {f : filter β} :
monotone g(uniformity α).lift (λ (s : set × α)), g (prod.swap ⁻¹' s)) f(uniformity α).lift g f

theorem uniformity_lift_le_comp {α : Type u_1} {β : Type u_2} [uniform_space α] {f : set × α)filter β} :
monotone f(uniformity α).lift (λ (s : set × α)), f (comp_rel s s)) (uniformity α).lift f

theorem comp_le_uniformity3 {α : Type u_1} [uniform_space α] :
(uniformity α).lift' (λ (s : set × α)), comp_rel s (comp_rel s s)) uniformity α

theorem comp_symm_mem_uniformity_sets {α : Type u_1} [uniform_space α] {s : set × α)} :
s uniformity α(∃ (t : set × α)) (H : t uniformity α), symmetric_rel t comp_rel t t s)

theorem subset_comp_self_of_mem_uniformity {α : Type u_1} [uniform_space α] {s : set × α)} :
s uniformity αs comp_rel s s

theorem comp_comp_symm_mem_uniformity_sets {α : Type u_1} [uniform_space α] {s : set × α)} :
s uniformity α(∃ (t : set × α)) (H : t uniformity α), symmetric_rel t comp_rel (comp_rel t t) t s)

 Balls in uniform spaces

def uniform_space.​ball {β : Type u_2} :
β → 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 mem_ball_comp {β : Type u_2} {V W : set × β)} {x y z : β} :

The triangle inequality for uniform_space.ball

theorem ball_subset_of_comp_subset {β : Type u_2} {V W : set × β)} {x y : β} :

theorem ball_mono {β : Type u_2} {V W : set × β)} (h : V W) (x : β) :

theorem mem_ball_symmetry {β : Type u_2} {V : set × β)} (hV : symmetric_rel V) {x y : β} :

theorem ball_eq_of_symmetry {β : Type u_2} {V : set × β)} (hV : symmetric_rel V) {x : β} :
uniform_space.ball x V = {y : β | (y, x) V}

theorem mem_comp_of_mem_ball {β : Type u_2} {V W : set × β)} {x y z : β} :

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} [uniform_space α] {x : α} {s : set α} :
s nhds x {p : α × α | p.fst = xp.snd s} uniformity α

theorem mem_nhds_uniformity_iff_left {α : Type u_1} [uniform_space α] {x : α} {s : set α} :
s nhds x {p : α × α | p.snd = xp.fst s} uniformity α

theorem nhds_eq_comap_uniformity_aux {α : Type u} {x : α} {s : set α} {F : filter × α)} :
{p : α × α | p.fst = xp.snd s} F s filter.comap (prod.mk x) F

theorem nhds_eq_comap_uniformity {α : Type u_1} [uniform_space α] {x : α} :

theorem is_open_iff_ball_subset {α : Type u_1} [uniform_space α] {s : set α} :
is_open s ∀ (x : α), x s(∃ (V : set × α)) (H : V uniformity α), uniform_space.ball x V s)

theorem nhds_basis_uniformity' {α : Type u_1} {β : Type u_2} [uniform_space α] {p : β → Prop} {s : β → set × α)} (h : (uniformity α).has_basis p s) {x : α} :
(nhds x).has_basis p (λ (i : β), {y : α | (x, y) s i})

theorem nhds_basis_uniformity {α : Type u_1} {β : Type u_2} [uniform_space α] {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} [uniform_space α] {x : α} {s : set α} :
s nhds x ∃ (V : set × α)) (H : V uniformity α), uniform_space.ball x V s

theorem uniform_space.​ball_mem_nhds {α : Type u_1} [uniform_space α] (x : α) ⦃V : set × α) :

theorem uniform_space.​mem_nhds_iff_symm {α : Type u_1} [uniform_space α] {x : α} {s : set α} :
s nhds x ∃ (V : set × α)) (H : V uniformity α), symmetric_rel V uniform_space.ball x V s

theorem uniform_space.​has_basis_nhds {α : Type u_1} [uniform_space α] (x : α) :
(nhds x).has_basis (λ (s : set × α)), s uniformity α symmetric_rel s) (λ (s : set × α)), uniform_space.ball x s)

theorem uniform_space.​has_basis_nhds_prod {α : Type u_1} [uniform_space α] (x y : α) :
(nhds (x, y)).has_basis (λ (s : set × α)), s uniformity α symmetric_rel s) (λ (s : set × α)), (uniform_space.ball x s).prod (uniform_space.ball y s))

theorem nhds_eq_uniformity {α : Type u_1} [uniform_space α] {x : α} :
nhds x = (uniformity α).lift' (λ (s : set × α)), {y : α | (x, y) s})

theorem mem_nhds_left {α : Type u_1} [uniform_space α] (x : α) {s : set × α)} :
s uniformity α{y : α | (x, y) s} nhds x

theorem mem_nhds_right {α : Type u_1} [uniform_space α] (y : α) {s : set × α)} :
s uniformity α{x : α | (x, y) s} nhds y

theorem tendsto_right_nhds_uniformity {α : Type u_1} [uniform_space α] {a : α} :
filter.tendsto (λ (a' : α), (a', a)) (nhds a) (uniformity α)

theorem tendsto_left_nhds_uniformity {α : Type u_1} [uniform_space α] {a : α} :
filter.tendsto (λ (a' : α), (a, a')) (nhds a) (uniformity α)

theorem lift_nhds_left {α : Type u_1} {β : Type u_2} [uniform_space α] {x : α} {g : set αfilter β} :
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} [uniform_space α] {x : α} {g : set αfilter β} :
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} [uniform_space α] {a b : α} :
(nhds a).prod (nhds b) = (uniformity α).lift (λ (s : set × α)), (uniformity α).lift' (λ (t : set × α)), {y : α | (y, a) s}.prod {y : α | (b, y) t}))

theorem nhds_eq_uniformity_prod {α : Type u_1} [uniform_space α] {a b : α} :
nhds (a, b) = (uniformity α).lift' (λ (s : set × α)), {y : α | (y, a) s}.prod {y : α | (b, y) s})

theorem nhdset_of_mem_uniformity {α : Type u_1} [uniform_space α] {d : set × α)} (s : set × α)) :
d uniformity α(∃ (t : set × α)), is_open t s t t {p : α × α | ∃ (x y : α), (p.fst, x) d (x, y) s (y, p.snd) d})

theorem nhds_le_uniformity {α : Type u_1} [uniform_space α] :
(⨆ (x : α), nhds (x, x)) uniformity α

Entourages are neighborhoods of the diagonal.

Closure and interior in uniform spaces

theorem closure_eq_uniformity {α : Type u_1} [uniform_space α] (s : set × α)) :
closure s = ⋂ (V : set × α)) (H : V {V : set × α) | V uniformity α symmetric_rel V}), comp_rel (comp_rel V s) V

theorem uniformity_has_basis_closed {α : Type u_1} [uniform_space α] :
(uniformity α).has_basis (λ (V : set × α)), V uniformity α is_closed V) id

theorem uniformity_has_basis_closure {α : Type u_1} [uniform_space α] :
(uniformity α).has_basis (λ (V : set × α)), V uniformity α) closure

Closed entourages form a basis of the uniformity filter.

theorem closure_eq_inter_uniformity {α : Type u_1} [uniform_space α] {t : set × α)} :
closure t = ⋂ (d : set × α)) (H : d uniformity α), comp_rel d (comp_rel t d)

theorem interior_mem_uniformity {α : Type u_1} [uniform_space α] {s : set × α)} :

theorem mem_uniformity_is_closed {α : Type u_1} [uniform_space α] {s : set × α)} :
s uniformity α(∃ (t : set × α)) (H : t uniformity α), is_closed t t s)

Uniformity bases

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

theorem uniform_space.​has_basis_symmetric {α : Type u_1} [uniform_space α] :
(uniformity α).has_basis (λ (s : set × α)), s uniformity α symmetric_rel s) id

Symmetric entourages form a basis of 𝓤 α

theorem uniform_space.​has_seq_basis {α : Type u_1} [uniform_space α] :
(uniformity α).is_countably_generated(∃ (V : set × α)), (uniformity α).has_antimono_basis (λ (_x : ), true) V ∀ (n : ), symmetric_rel (V n))

Uniform continuity

def uniform_continuous {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :
(α → β) → 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
def uniform_continuous_on {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :
(α → β)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.prod 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} [uniform_space α] [uniform_space β] {f : α → β} :
uniform_continuous f ∀ (r : set × β)), r uniformity β{x : α × α | (f x.fst, f x.snd) r} uniformity α

theorem uniform_continuous_iff_eventually {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} :
uniform_continuous f ∀ (r : set × β)), r uniformity β(∀ᶠ (x : α × α) in uniformity α, (f x.fst, f x.snd) r)

theorem uniform_continuous_of_const {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {c : α → β} :
(∀ (a b : α), c a = c b)uniform_continuous c

theorem uniform_continuous_const {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {b : β} :
uniform_continuous (λ (a : α), b)

theorem uniform_continuous.​comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {g : β → γ} {f : α → β} :

theorem filter.​has_basis.​uniform_continuous_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [uniform_space α] [uniform_space β] {p : γ → Prop} {s : γ → set × α)} (ha : (uniformity α).has_basis p s) {q : δ → Prop} {t : δ → set × β)} (hb : (uniformity β).has_basis q t) {f : α → β} :
uniform_continuous f ∀ (i : δ), q i(∃ (j : γ) (hj : p j), ∀ (x y : α), (x, y) s j(f x, f y) t i)

@[instance]
def uniform_space.​has_Inf {α : Type u_1} :

Equations
@[instance]
def uniform_space.​has_top {α : Type u_1} :

Equations
@[instance]

Equations
theorem infi_uniformity {α : Type u_1} {ι : Sort u_2} {u : ι → uniform_space α} :

@[instance]
def inhabited_uniform_space {α : Type u_1} :

Equations
def uniform_space.​comap {α : Type u_1} {β : Type u_2} :
(α → β)uniform_space β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} [uniform_space α] [uniform_space β] {f : α → β} :
_inst_1 = uniform_space.comap f _inst_2uniformity α = filter.comap (prod.map f f) (uniformity β)

theorem uniform_space.​comap_comap {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uγ : uniform_space γ] {f : α → β} {g : β → γ} :

theorem uniform_continuous_iff {α : Type u_1} {β : Type u_2} [uα : uniform_space α] [uβ : uniform_space β] {f : α → β} :

theorem uniform_continuous_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 α] :

theorem uniform_continuous.​continuous {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} :

theorem to_topological_space_infi {α : Type u_1} {ι : Sort u_2} {u : ι → uniform_space α} :

@[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 α] :

theorem uniform_continuous_subtype_val {α : Type u_1} {p : α → Prop} [uniform_space α] :

theorem uniform_continuous_subtype_mk {α : Type u_1} {β : Type u_2} {p : α → Prop} [uniform_space α] [uniform_space β] {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} [uniform_space α] [uniform_space β] (f : α → β) (s : set α) :

theorem tendsto_of_uniform_continuous_subtype {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} {s : set α} {a : α} :
uniform_continuous (λ (x : s), f x.val)s nhds afilter.tendsto f (nhds a) (nhds (f a))

@[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} [uniform_space α] [uniform_space β] :
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} [uniform_space α] [uniform_space β] :
uniformity × β) = filter.map (λ (p : × α) × β × β), ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ((uniformity α).prod (uniformity β))

theorem mem_map_sets_iff' {α : Type u_1} {β : Type u_2} {f : filter α} {m : α → β} {t : set β} :
t (filter.map m f).sets ∃ (s : set α) (H : s f), m '' s t

theorem mem_uniformity_of_uniform_continuous_invariant {α : Type u_1} [uniform_space α] {s : set × α)} {f : α → α → α} :
uniform_continuous (λ (p : α × α), f p.fst p.snd)s uniformity α(∃ (u : set × α)) (H : u uniformity α), ∀ (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 × β)} :
a uniformity αb uniformity β{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} [uniform_space α] [uniform_space β] :
filter.tendsto (λ (p : × β) × α × β), (p.fst.fst, p.snd.fst)) (uniformity × β)) (uniformity α)

theorem tendsto_prod_uniformity_snd {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :
filter.tendsto (λ (p : × β) × α × β), (p.fst.snd, p.snd.snd)) (uniformity × β)) (uniformity β)

theorem uniform_continuous_fst {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :
uniform_continuous (λ (p : α × β), p.fst)

theorem uniform_continuous_snd {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :
uniform_continuous (λ (p : α × β), p.snd)

theorem uniform_continuous.​prod_mk {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {f₁ : α → β} {f₂ : α → γ} :
uniform_continuous f₁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} [uniform_space α] [uniform_space β] [uniform_space γ] {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} [uniform_space α] [uniform_space β] [uniform_space γ] {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} [uniform_space α] [uniform_space β] [uniform_space γ] [uniform_space δ] {f : α → γ} {g : β → δ} :

def uniform_continuous₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] :
(α → β → γ) → Prop

Uniform continuity for functions of two variables.

Equations
theorem uniform_continuous₂_def {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] (f : α → β → γ) :

theorem uniform_continuous₂.​uniform_continuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] {f : α → β → γ} :

theorem uniform_continuous₂_curry {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [uniform_space γ] (f : α × β → γ) :

theorem uniform_continuous₂.​comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [uniform_space α] [uniform_space β] [uniform_space γ] [uniform_space δ] {f : α → β → γ} {g : γ → δ} :

theorem uniform_continuous₂.​bicompl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {δ' : Type u_6} [uniform_space α] [uniform_space β] [uniform_space γ] [uniform_space δ] [uniform_space δ'] {f : α → β → γ} {ga : δ → α} {gb : δ' → β} :

def uniform_space.​core.​sum {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :

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} [uniform_space α] [uniform_space β] {a : set × α)} (ha : a uniformity α) {b : set × β)} :
b uniformity β(λ (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} [uniform_space α] [uniform_space β] {s : set β)} (hs : is_open s) {x : α β} :
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} [uniform_space α] [uniform_space β] {s : set β)} :
(∀ (x : α β), x s{p : β) × β) | p.fst = xp.snd s} uniform_space.core.sum.uniformity)is_open s

theorem sum.​uniformity {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] :
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} [uniform_space α] {s : set α} {ι : Sort u_1} {c : ι → set α} :
is_compact s(∀ (i : ι), is_open (c i))(s ⋃ (i : ι), c i)(∃ (n : set × α)) (H : n uniformity α), ∀ (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} [uniform_space α] {s : set α} {c : set (set α)} :
is_compact s(∀ (t : set α), t cis_open t)s ⋃₀c(∃ (n : set × α)) (H : n uniformity α), ∀ (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.

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} [uniform_space α] {f : filter β} {u : β → α} {a : α} :
filter.tendsto u f (nhds a) filter.tendsto (λ (x : β), (a, u x)) f (uniformity α)

theorem uniform.​tendsto_nhds_left {α : Type u_1} {β : Type u_2} [uniform_space α] {f : filter β} {u : β → α} {a : α} :
filter.tendsto u f (nhds a) filter.tendsto (λ (x : β), (u x, a)) f (uniformity α)

theorem uniform.​continuous_at_iff'_right {α : Type u_1} {β : Type u_2} [uniform_space α] [topological_space β] {f : β → α} {b : β} :
continuous_at f b filter.tendsto (λ (x : β), (f b, f x)) (nhds b) (uniformity α)

theorem uniform.​continuous_at_iff'_left {α : Type u_1} {β : Type u_2} [uniform_space α] [topological_space β] {f : β → α} {b : β} :
continuous_at f b filter.tendsto (λ (x : β), (f x, f b)) (nhds b) (uniformity α)

theorem uniform.​continuous_within_at_iff'_right {α : Type u_1} {β : Type u_2} [uniform_space α] [topological_space β] {f : β → α} {b : β} {s : set β} :
continuous_within_at f s b filter.tendsto (λ (x : β), (f b, f x)) (nhds_within b s) (uniformity α)

theorem uniform.​continuous_within_at_iff'_left {α : Type u_1} {β : Type u_2} [uniform_space α] [topological_space β] {f : β → α} {b : β} {s : set β} :
continuous_within_at f s b filter.tendsto (λ (x : β), (f x, f b)) (nhds_within b s) (uniformity α)

theorem uniform.​continuous_on_iff'_right {α : Type u_1} {β : Type u_2} [uniform_space α] [topological_space β] {f : β → α} {s : set β} :
continuous_on f s ∀ (b : β), b sfilter.tendsto (λ (x : β), (f b, f x)) (nhds_within b s) (uniformity α)

theorem uniform.​continuous_on_iff'_left {α : Type u_1} {β : Type u_2} [uniform_space α] [topological_space β] {f : β → α} {s : set β} :
continuous_on f s ∀ (b : β), b sfilter.tendsto (λ (x : β), (f x, f b)) (nhds_within b s) (uniformity α)

theorem uniform.​continuous_iff'_right {α : Type u_1} {β : Type u_2} [uniform_space α] [topological_space β] {f : β → α} :
continuous f ∀ (b : β), filter.tendsto (λ (x : β), (f b, f x)) (nhds b) (uniformity α)

theorem uniform.​continuous_iff'_left {α : Type u_1} {β : Type u_2} [uniform_space α] [topological_space β] {f : β → α} :
continuous f ∀ (b : β), filter.tendsto (λ (x : β), (f x, f b)) (nhds b) (uniformity α)

theorem filter.​tendsto.​congr_uniformity {α : Type u_1} {β : Type u_2} [uniform_space β] {f g : α → β} {l : filter α} {b : β} :
filter.tendsto f l (nhds b)filter.tendsto (λ (x : α), (f x, g x)) l (uniformity β)filter.tendsto g l (nhds b)

theorem uniform.​tendsto_congr {α : Type u_1} {β : Type u_2} [uniform_space β] {f g : α → β} {l : filter α} {b : β} :
filter.tendsto (λ (x : α), (f x, g x)) l (uniformity β)(filter.tendsto f l (nhds b) filter.tendsto g l (nhds b))