# 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 UniformEmbedding.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

In this file we also define a complete lattice structure on the type UniformSpace X of uniform structures on X, as well as the pullback (UniformSpace.comap) of uniform structures coming from the pullback of filters. Like distance functions, uniform structures cannot be pushed forward in general.

## Notations #

Localized in Uniformity, we have the notation 𝓤 X for the uniformity on a uniform space X, and ○ for composition of relations, seen as terms with type Set (X × X).

## Implementation notes #

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

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

## References #

The formalization uses the books:

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

### Relations, seen as Set (α × α)#

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

The identity relation, or the graph of the identity function

Equations
• idRel = {p : α × α | p.1 = p.2}
Instances For
@[simp]
theorem mem_idRel {α : Type ua} {a : α} {b : α} :
(a, b) idRel a = b
@[simp]
theorem idRel_subset {α : Type ua} {s : Set (α × α)} :
idRel s ∀ (a : α), (a, a) s
def compRel {α : Type ua} (r₁ : Set (α × α)) (r₂ : Set (α × α)) :
Set (α × α)

The composition of relations

Equations
Instances For

The composition of relations

Equations
Instances For
@[simp]
theorem mem_compRel {α : Type u} {r₁ : Set (α × α)} {r₂ : Set (α × α)} {x : α} {y : α} :
(x, y) compRel r₁ r₂ ∃ (z : α), (x, z) r₁ (z, y) r₂
@[simp]
theorem swap_idRel {α : Type ua} :
Prod.swap '' idRel = idRel
theorem Monotone.compRel {α : Type ua} {β : Type ub} [] {f : βSet (α × α)} {g : βSet (α × α)} (hf : ) (hg : ) :
Monotone fun (x : β) => compRel (f x) (g x)
theorem compRel_mono {α : Type ua} {f : Set (α × α)} {g : Set (α × α)} {h : Set (α × α)} {k : Set (α × α)} (h₁ : f h) (h₂ : g k) :
theorem prod_mk_mem_compRel {α : Type ua} {a : α} {b : α} {c : α} {s : Set (α × α)} {t : Set (α × α)} (h₁ : (a, c) s) (h₂ : (c, b) t) :
(a, b) compRel s t
@[simp]
theorem id_compRel {α : Type ua} {r : Set (α × α)} :
compRel idRel r = r
theorem compRel_assoc {α : Type ua} {r : Set (α × α)} {s : Set (α × α)} {t : Set (α × α)} :
compRel (compRel r s) t = compRel r (compRel s t)
theorem left_subset_compRel {α : Type ua} {s : Set (α × α)} {t : Set (α × α)} (h : idRel t) :
s compRel s t
theorem right_subset_compRel {α : Type ua} {s : Set (α × α)} {t : Set (α × α)} (h : idRel s) :
t compRel s t
theorem subset_comp_self {α : Type ua} {s : Set (α × α)} (h : idRel s) :
s compRel s s
theorem subset_iterate_compRel {α : Type ua} {s : Set (α × α)} {t : Set (α × α)} (h : idRel s) (n : ) :
t (fun (x : Set (α × α)) => compRel s x)^[n] t
def SymmetricRel {α : Type ua} (V : Set (α × α)) :

The relation is invariant under swapping factors.

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

The maximal symmetric relation contained in a given relation.

Equations
Instances For
theorem symmetric_symmetrizeRel {α : Type ua} (V : Set (α × α)) :
theorem symmetrizeRel_subset_self {α : Type ua} (V : Set (α × α)) :
theorem symmetrize_mono {α : Type ua} {V : Set (α × α)} {W : Set (α × α)} (h : V W) :
theorem SymmetricRel.mk_mem_comm {α : Type ua} {V : Set (α × α)} (hV : ) {x : α} {y : α} :
(x, y) V (y, x) V
theorem SymmetricRel.eq {α : Type ua} {U : Set (α × α)} (hU : ) :
Prod.swap ⁻¹' U = U
theorem SymmetricRel.inter {α : Type ua} {U : Set (α × α)} {V : Set (α × α)} (hU : ) (hV : ) :
structure UniformSpace.Core (α : Type u) :

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

• uniformity : Filter (α × α)

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

• refl : Filter.principal idRel self.uniformity

Every set in the uniformity filter includes the diagonal.

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

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

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

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

Instances For
theorem UniformSpace.Core.refl {α : Type u} (self : ) :
Filter.principal idRel self.uniformity

Every set in the uniformity filter includes the diagonal.

theorem UniformSpace.Core.symm {α : Type u} (self : ) :
Filter.Tendsto Prod.swap self.uniformity self.uniformity

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

theorem UniformSpace.Core.comp {α : Type u} (self : ) :
(self.uniformity.lift' fun (s : Set (α × α)) => compRel s s) self.uniformity

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

theorem UniformSpace.Core.comp_mem_uniformity_sets {α : Type ua} {c : } {s : Set (α × α)} (hs : s c.uniformity) :
tc.uniformity, compRel t t s
def UniformSpace.Core.mk' {α : Type u} (U : Filter (α × α)) (refl : rU, ∀ (x : α), (x, x) r) (symm : rU, Prod.swap ⁻¹' r U) (comp : rU, tU, compRel t t r) :

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

Equations
Instances For
def UniformSpace.Core.mkOfBasis {α : Type u} (B : FilterBasis (α × α)) (refl : rB, ∀ (x : α), (x, x) r) (symm : rB, tB, t Prod.swap ⁻¹' r) (comp : rB, tB, compRel t t r) :

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

Equations
Instances For

A uniform space generates a topological space

Equations
Instances For
theorem UniformSpace.Core.ext {α : Type ua} {u₁ : } {u₂ : } :
u₁.uniformity = u₂.uniformityu₁ = u₂
theorem UniformSpace.Core.nhds_toTopologicalSpace {α : Type u} (u : ) (x : α) :
nhds x = Filter.comap () u.uniformity
class UniformSpace (α : Type u) extends :

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 α),
• isOpen_sUnion : ∀ (s : Set (Set α)), (ts, )
• uniformity : Filter (α × α)

The uniformity filter.

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

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

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

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

• nhds_eq_comap_uniformity : ∀ (x : α), nhds x = Filter.comap () UniformSpace.uniformity

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

Instances
theorem UniformSpace.symm {α : Type u} [self : ] :
Filter.Tendsto Prod.swap UniformSpace.uniformity UniformSpace.uniformity

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

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

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

theorem UniformSpace.nhds_eq_comap_uniformity {α : Type u} [self : ] (x : α) :
nhds x = Filter.comap () UniformSpace.uniformity

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

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

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

Equations
• = UniformSpace.uniformity
Instances For

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

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

Equations
Instances For
@[reducible, inline]
abbrev UniformSpace.ofCoreEq {α : Type u} (u : ) (t : ) (h : t = u.toTopologicalSpace) :

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

Equations
Instances For
@[reducible, inline]
abbrev UniformSpace.ofCore {α : Type u} (u : ) :

Construct a UniformSpace from a UniformSpace.Core.

Equations
Instances For
@[reducible, inline]
abbrev UniformSpace.toCore {α : Type ua} (u : ) :

Construct a UniformSpace.Core from a UniformSpace.

Equations
• u.toCore = let __spread.0 := u; { uniformity := UniformSpace.uniformity, refl := , symm := , comp := }
Instances For
theorem UniformSpace.toCore_toTopologicalSpace {α : Type ua} (u : ) :
u.toCore.toTopologicalSpace = UniformSpace.toTopologicalSpace
@[deprecated UniformSpace.mk]
def UniformSpace.ofNhdsEqComap {α : Type ua} (u : ) (_t : ) (h : ∀ (x : α), nhds x = Filter.comap () u.uniformity) :

Build a UniformSpace from a UniformSpace.Core and a compatible topology. Use UniformSpace.mk instead to avoid proving the unnecessary assumption UniformSpace.Core.refl.

The main constructor used to use a different compatibility assumption. This definition was created as a step towards porting to a new definition. Now the main definition is ported, so this constructor will be removed in a few months.

Equations
Instances For
theorem UniformSpace.ext {α : Type ua} {u₁ : } {u₂ : } (h : ) :
u₁ = u₂
theorem UniformSpace.ext_iff {α : Type ua} {u₁ : } {u₂ : } :
u₁ = u₂ ∀ (s : Set (α × α)), s s
theorem UniformSpace.ofCoreEq_toCore {α : Type ua} (u : ) (t : ) (h : t = u.toCore.toTopologicalSpace) :
UniformSpace.ofCoreEq u.toCore t h = u
@[reducible, inline]
abbrev UniformSpace.replaceTopology {α : Type u_2} [i : ] (u : ) (h : i = UniformSpace.toTopologicalSpace) :

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

Equations
• u.replaceTopology h = let __spread.0 := u; UniformSpace.mk UniformSpace.uniformity
Instances For
theorem UniformSpace.replaceTopology_eq {α : Type u_2} [i : ] (u : ) (h : i = UniformSpace.toTopologicalSpace) :
u.replaceTopology h = u
def UniformSpace.ofFun {α : Type u} {β : Type v} (d : ααβ) (refl : ∀ (x : α), d x x = 0) (symm : ∀ (x y : α), d x y = d y x) (triangle : ∀ (x y z : α), d x z d x y + d y z) (half : ε > 0, δ > 0, x < δ, y < δ, x + y < ε) :

Define a UniformSpace using a "distance" function. The function can be, e.g., the distance in a (usual or extended) metric space or an absolute value on a ring.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem UniformSpace.hasBasis_ofFun {α : Type u} {β : Type v} (h₀ : ∃ (x : β), 0 < x) (d : ααβ) (refl : ∀ (x : α), d x x = 0) (symm : ∀ (x y : α), d x y = d y x) (triangle : ∀ (x y z : α), d x z d x y + d y z) (half : ε > 0, δ > 0, x < δ, y < δ, x + y < ε) :
().HasBasis (fun (x : β) => 0 < x) fun (ε : β) => {x : α × α | d x.1 x.2 < ε}
theorem nhds_eq_comap_uniformity {α : Type ua} [] {x : α} :
theorem isOpen_uniformity {α : Type ua} [] {s : Set α} :
xs, {p : α × α | p.1 = xp.2 s}
theorem refl_le_uniformity {α : Type ua} [] :
instance uniformity.neBot {α : Type ua} [] [] :
().NeBot
Equations
• =
theorem refl_mem_uniformity {α : Type ua} [] {x : α} {s : Set (α × α)} (h : s ) :
(x, x) s
theorem mem_uniformity_of_eq {α : Type ua} [] {x : α} {y : α} {s : Set (α × α)} (h : s ) (hx : x = y) :
(x, y) s
theorem symm_le_uniformity {α : Type ua} [] :
Filter.map Prod.swap ()
theorem comp_le_uniformity {α : Type ua} [] :
(().lift' fun (s : Set (α × α)) => compRel s s)
theorem lift'_comp_uniformity {α : Type ua} [] :
(().lift' fun (s : Set (α × α)) => compRel s s) =
theorem tendsto_swap_uniformity {α : Type ua} [] :
Filter.Tendsto Prod.swap () ()
theorem comp_mem_uniformity_sets {α : Type ua} [] {s : Set (α × α)} (hs : s ) :
t, compRel t t s
theorem eventually_uniformity_iterate_comp_subset {α : Type ua} [] {s : Set (α × α)} (hs : s ) (n : ) :
∀ᶠ (t : Set (α × α)) in ().smallSets, (fun (x : Set (α × α)) => compRel t x)^[n] t s

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

theorem eventually_uniformity_comp_subset {α : Type ua} [] {s : Set (α × α)} (hs : s ) :
∀ᶠ (t : Set (α × α)) in ().smallSets, compRel t t s

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

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

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

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

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

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

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

theorem tendsto_const_uniformity {α : Type ua} {β : Type ub} [] {a : α} {f : } :
Filter.Tendsto (fun (x : β) => (a, a)) f ()
theorem symm_of_uniformity {α : Type ua} [] {s : Set (α × α)} (hs : s ) :
t, (∀ (a b : α), (a, b) t(b, a) t) t s
theorem comp_symm_of_uniformity {α : Type ua} [] {s : Set (α × α)} (hs : s ) :
t, (∀ {a b : α}, (a, b) t(b, a) t) compRel t t s
theorem uniformity_le_symm {α : Type ua} [] :
Prod.swap <$> theorem uniformity_eq_symm {α : Type ua} [] : = Prod.swap <$>
@[simp]
theorem comap_swap_uniformity {α : Type ua} [] :
Filter.comap Prod.swap () =
theorem symmetrize_mem_uniformity {α : Type ua} [] {V : Set (α × α)} (h : V ) :
theorem UniformSpace.hasBasis_symmetric {α : Type ua} [] :
().HasBasis (fun (s : Set (α × α)) => s ) id

Symmetric entourages form a basis of 𝓤 α

theorem uniformity_lift_le_swap {α : Type ua} {β : Type ub} [] {g : Set (α × α)} {f : } (hg : ) (h : (().lift fun (s : Set (α × α)) => g (Prod.swap ⁻¹' s)) f) :
().lift g f
theorem uniformity_lift_le_comp {α : Type ua} {β : Type ub} [] {f : Set (α × α)} (h : ) :
(().lift fun (s : Set (α × α)) => f (compRel s s)) ().lift f
theorem comp3_mem_uniformity {α : Type ua} [] {s : Set (α × α)} (hs : s ) :
t, compRel t (compRel t t) s
theorem comp_le_uniformity3 {α : Type ua} [] :
(().lift' fun (s : Set (α × α)) => compRel s (compRel s s))

See also comp3_mem_uniformity.

theorem comp_symm_mem_uniformity_sets {α : Type ua} [] {s : Set (α × α)} (hs : s ) :
t, compRel t t s

See also comp_open_symm_mem_uniformity_sets.

theorem subset_comp_self_of_mem_uniformity {α : Type ua} [] {s : Set (α × α)} (h : s ) :
s compRel s s
theorem comp_comp_symm_mem_uniformity_sets {α : Type ua} [] {s : Set (α × α)} (hs : s ) :
t, compRel (compRel t t) t s

### Balls in uniform spaces #

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

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

Equations
Instances For
theorem UniformSpace.mem_ball_self {α : Type ua} [] (x : α) {V : Set (α × α)} (hV : V ) :
x
theorem mem_ball_comp {β : Type ub} {V : Set (β × β)} {W : Set (β × β)} {x : β} {y : β} {z : β} (h : y ) (h' : z ) :

The triangle inequality for UniformSpace.ball

theorem ball_subset_of_comp_subset {β : Type ub} {V : Set (β × β)} {W : Set (β × β)} {x : β} {y : β} (h : x ) (h' : compRel W W V) :
theorem ball_mono {β : Type ub} {V : Set (β × β)} {W : Set (β × β)} (h : V W) (x : β) :
theorem ball_inter {β : Type ub} (x : β) (V : Set (β × β)) (W : Set (β × β)) :
theorem ball_inter_left {β : Type ub} (x : β) (V : Set (β × β)) (W : Set (β × β)) :
theorem ball_inter_right {β : Type ub} (x : β) (V : Set (β × β)) (W : Set (β × β)) :
theorem mem_ball_symmetry {β : Type ub} {V : Set (β × β)} (hV : ) {x : β} {y : β} :
x y
theorem ball_eq_of_symmetry {β : Type ub} {V : Set (β × β)} (hV : ) {x : β} :
= {y : β | (y, x) V}
theorem mem_comp_of_mem_ball {β : Type ub} {V : Set (β × β)} {W : Set (β × β)} {x : β} {y : β} {z : β} (hV : ) (hx : x ) (hy : y ) :
(x, y) compRel V W
theorem UniformSpace.isOpen_ball {α : Type ua} [] (x : α) {V : Set (α × α)} (hV : ) :
theorem UniformSpace.isClosed_ball {α : Type ua} [] (x : α) {V : Set (α × α)} (hV : ) :
theorem mem_comp_comp {β : Type ub} {V : Set (β × β)} {W : Set (β × β)} {M : Set (β × β)} (hW' : ) {p : β × β} :
p compRel (compRel V M) W ( ×ˢ M).Nonempty

### Neighborhoods in uniform spaces #

theorem mem_nhds_uniformity_iff_right {α : Type ua} [] {x : α} {s : Set α} :
s nhds x {p : α × α | p.1 = xp.2 s}
theorem mem_nhds_uniformity_iff_left {α : Type ua} [] {x : α} {s : Set α} :
s nhds x {p : α × α | p.2 = xp.1 s}
theorem nhdsWithin_eq_comap_uniformity_of_mem {α : Type ua} [] {x : α} {T : Set α} (hx : x T) (S : Set α) :
theorem nhdsWithin_eq_comap_uniformity {α : Type ua} [] {x : α} (S : Set α) :
= Filter.comap () ( Filter.principal (Set.univ ×ˢ S))
theorem isOpen_iff_ball_subset {α : Type ua} [] {s : Set α} :
xs, V, s

See also isOpen_iff_open_ball_subset.

theorem nhds_basis_uniformity' {α : Type ua} {ι : Sort u_1} [] {p : ιProp} {s : ιSet (α × α)} (h : ().HasBasis p s) {x : α} :
(nhds x).HasBasis p fun (i : ι) => UniformSpace.ball x (s i)
theorem nhds_basis_uniformity {α : Type ua} {ι : Sort u_1} [] {p : ιProp} {s : ιSet (α × α)} (h : ().HasBasis p s) {x : α} :
(nhds x).HasBasis p fun (i : ι) => {y : α | (y, x) s i}
theorem nhds_eq_comap_uniformity' {α : Type ua} [] {x : α} :
nhds x = Filter.comap (fun (y : α) => (y, x)) ()
theorem UniformSpace.mem_nhds_iff {α : Type ua} [] {x : α} {s : Set α} :
s nhds x V, s
theorem UniformSpace.ball_mem_nhds {α : Type ua} [] (x : α) ⦃V : Set (α × α) (V_in : V ) :
theorem UniformSpace.ball_mem_nhdsWithin {α : Type ua} [] {x : α} {S : Set α} ⦃V : Set (α × α) (x_in : x S) (V_in : V Filter.principal (S ×ˢ S)) :
theorem UniformSpace.mem_nhds_iff_symm {α : Type ua} [] {x : α} {s : Set α} :
s nhds x V, s
theorem UniformSpace.hasBasis_nhds {α : Type ua} [] (x : α) :
(nhds x).HasBasis (fun (s : Set (α × α)) => s ) fun (s : Set (α × α)) =>
theorem UniformSpace.mem_closure_iff_symm_ball {α : Type ua} [] {s : Set α} {x : α} :
x ∀ {V : Set (α × α)}, V (s ).Nonempty
theorem UniformSpace.mem_closure_iff_ball {α : Type ua} [] {s : Set α} {x : α} :
x ∀ {V : Set (α × α)}, V ( s).Nonempty
theorem UniformSpace.hasBasis_nhds_prod {α : Type ua} [] (x : α) (y : α) :
(nhds (x, y)).HasBasis (fun (s : Set (α × α)) => s ) fun (s : Set (α × α)) =>
theorem nhds_eq_uniformity {α : Type ua} [] {x : α} :
nhds x = ().lift'
theorem nhds_eq_uniformity' {α : Type ua} [] {x : α} :
nhds x = ().lift' fun (s : Set (α × α)) => {y : α | (y, x) s}
theorem mem_nhds_left {α : Type ua} [] (x : α) {s : Set (α × α)} (h : s ) :
{y : α | (x, y) s} nhds x
theorem mem_nhds_right {α : Type ua} [] (y : α) {s : Set (α × α)} (h : s ) :
{x : α | (x, y) s} nhds y
theorem exists_mem_nhds_ball_subset_of_mem_nhds {α : Type ua} [] {a : α} {U : Set α} (h : U nhds a) :
Vnhds a, t, a'V, U
theorem tendsto_right_nhds_uniformity {α : Type ua} [] {a : α} :
Filter.Tendsto (fun (a' : α) => (a', a)) (nhds a) ()
theorem tendsto_left_nhds_uniformity {α : Type ua} [] {a : α} :
Filter.Tendsto (fun (a' : α) => (a, a')) (nhds a) ()
theorem lift_nhds_left {α : Type ua} {β : Type ub} [] {x : α} {g : Set α} (hg : ) :
(nhds x).lift g = ().lift fun (s : Set (α × α)) => g ()
theorem lift_nhds_right {α : Type ua} {β : Type ub} [] {x : α} {g : Set α} (hg : ) :
(nhds x).lift g = ().lift fun (s : Set (α × α)) => g {y : α | (y, x) s}
theorem nhds_nhds_eq_uniformity_uniformity_prod {α : Type ua} [] {a : α} {b : α} :
nhds a ×ˢ nhds b = ().lift fun (s : Set (α × α)) => ().lift' fun (t : Set (α × α)) => {y : α | (y, a) s} ×ˢ {y : α | (b, y) t}
theorem nhds_eq_uniformity_prod {α : Type ua} [] {a : α} {b : α} :
nhds (a, b) = ().lift' fun (s : Set (α × α)) => {y : α | (y, a) s} ×ˢ {y : α | (b, y) s}
theorem nhdset_of_mem_uniformity {α : Type ua} [] {d : Set (α × α)} (s : Set (α × α)) (hd : d ) :
∃ (t : Set (α × α)), s t t {p : α × α | ∃ (x : α) (y : α), (p.1, x) d (x, y) s (y, p.2) d}
theorem nhds_le_uniformity {α : Type ua} [] (x : α) :
nhds (x, x)

Entourages are neighborhoods of the diagonal.

theorem iSup_nhds_le_uniformity {α : Type ua} [] :
⨆ (x : α), nhds (x, x)

Entourages are neighborhoods of the diagonal.

theorem nhdsSet_diagonal_le_uniformity {α : Type ua} [] :

Entourages are neighborhoods of the diagonal.

### Closure and interior in uniform spaces #

theorem closure_eq_uniformity {α : Type ua} [] (s : Set (α × α)) :
= V{V : Set (α × α) | V }, compRel (compRel V s) V
theorem uniformity_hasBasis_closed {α : Type ua} [] :
().HasBasis (fun (V : Set (α × α)) => V ) id
theorem uniformity_eq_uniformity_closure {α : Type ua} [] :
= ().lift' closure
theorem Filter.HasBasis.uniformity_closure {α : Type ua} {ι : Sort u_1} [] {p : ιProp} {U : ιSet (α × α)} (h : ().HasBasis p U) :
().HasBasis p fun (i : ι) => closure (U i)
theorem uniformity_hasBasis_closure {α : Type ua} [] :
().HasBasis (fun (V : Set (α × α)) => V ) closure

Closed entourages form a basis of the uniformity filter.

theorem closure_eq_inter_uniformity {α : Type ua} [] {t : Set (α × α)} :
= d, compRel d (compRel t d)
theorem uniformity_eq_uniformity_interior {α : Type ua} [] :
= ().lift' interior
theorem interior_mem_uniformity {α : Type ua} [] {s : Set (α × α)} (hs : s ) :
theorem mem_uniformity_isClosed {α : Type ua} [] {s : Set (α × α)} (h : s ) :
t, t s
theorem isOpen_iff_open_ball_subset {α : Type ua} [] {s : Set α} :
xs, V, s
theorem Dense.biUnion_uniformity_ball {α : Type ua} [] {s : Set α} {U : Set (α × α)} (hs : ) (hU : U ) :
xs, = Set.univ

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

theorem DenseRange.iUnion_uniformity_ball {α : Type ua} [] {ι : Type u_2} {xs : ια} (xs_dense : ) {U : Set (α × α)} (hU : U ) :
⋃ (i : ι), UniformSpace.ball (xs i) U = Set.univ

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

### Uniformity bases #

theorem uniformity_hasBasis_open {α : Type ua} [] :
().HasBasis (fun (V : Set (α × α)) => V ) id

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

theorem Filter.HasBasis.mem_uniformity_iff {α : Type ua} {β : Type ub} [] {p : βProp} {s : βSet (α × α)} (h : ().HasBasis p s) {t : Set (α × α)} :
t ∃ (i : β), p i ∀ (a b : α), (a, b) s i(a, b) t
theorem uniformity_hasBasis_open_symmetric {α : Type ua} [] :
().HasBasis (fun (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 ua} [] {s : Set (α × α)} (hs : s ) :
t, compRel t t s
theorem UniformSpace.has_seq_basis (α : Type ua) [] [().IsCountablyGenerated] :
∃ (V : Set (α × α)), ().HasAntitoneBasis V ∀ (n : ), SymmetricRel (V n)
theorem Filter.HasBasis.biInter_biUnion_ball {α : Type ua} {ι : Sort u_1} [] {p : ιProp} {U : ιSet (α × α)} (h : ().HasBasis p U) (s : Set α) :
⋂ (i : ι), ⋂ (_ : p i), xs, UniformSpace.ball x (U i) =

### Uniform continuity #

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

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

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
def UniformContinuousOn {α : Type ua} {β : Type ub} [] [] (f : αβ) (s : Set α) :

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
Instances For
theorem uniformContinuous_def {α : Type ua} {β : Type ub} [] [] {f : αβ} :
r, {x : α × α | (f x.1, f x.2) r}
theorem uniformContinuous_iff_eventually {α : Type ua} {β : Type ub} [] [] {f : αβ} :
r, ∀ᶠ (x : α × α) in , (f x.1, f x.2) r
theorem uniformContinuousOn_univ {α : Type ua} {β : Type ub} [] [] {f : αβ} :
theorem uniformContinuous_of_const {α : Type ua} {β : Type ub} [] [] {c : αβ} (h : ∀ (a b : α), c a = c b) :
theorem uniformContinuous_id {α : Type ua} [] :
theorem uniformContinuous_const {α : Type ua} {β : Type ub} [] [] {b : β} :
UniformContinuous fun (x : α) => b
theorem UniformContinuous.comp {α : Type ua} {β : Type ub} {γ : Type uc} [] [] [] {g : βγ} {f : αβ} (hg : ) (hf : ) :
theorem UniformContinuous.iterate {β : Type ub} [] (T : ββ) (n : ) (h : ) :

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

theorem Filter.HasBasis.uniformContinuous_iff {α : Type ua} {β : Type ub} {ι : Sort u_1} [] {ι' : Sort u_2} [] {p : ιProp} {s : ιSet (α × α)} (ha : ().HasBasis p s) {q : ι'Prop} {t : ι'Set (β × β)} (hb : ().HasBasis q t) {f : αβ} :
∀ (i : ι'), q i∃ (j : ι), p j ∀ (x y : α), (x, y) s j(f x, f y) t i
theorem Filter.HasBasis.uniformContinuousOn_iff {α : Type ua} {β : Type ub} {ι : Sort u_1} [] {ι' : Sort u_2} [] {p : ιProp} {s : ιSet (α × α)} (ha : ().HasBasis p s) {q : ι'Prop} {t : ι'Set (β × β)} (hb : ().HasBasis q t) {f : αβ} {S : Set α} :
∀ (i : ι'), q i∃ (j : ι), p j xS, yS, (x, y) s j(f x, f y) t i
instance instPartialOrderUniformSpace {α : Type ua} :
Equations
theorem UniformSpace.le_def {α : Type ua} {u₁ : } {u₂ : } :
u₁ u₂
instance instInfSetUniformSpace {α : Type ua} :
Equations
• instInfSetUniformSpace = { sInf := fun (s : Set ()) => UniformSpace.ofCore { uniformity := us, , refl := , symm := , comp := } }
theorem UniformSpace.sInf_le {α : Type ua} {tt : Set ()} {t : } (h : t tt) :
sInf tt t
theorem UniformSpace.le_sInf {α : Type ua} {tt : Set ()} {t : } (h : t'tt, t t') :
t sInf tt
instance instTopUniformSpace {α : Type ua} :
Top ()
Equations
• instTopUniformSpace = { top := }
instance instBotUniformSpace {α : Type ua} :
Bot ()
Equations
instance instInfUniformSpace {α : Type ua} :
Inf ()
Equations
• instInfUniformSpace = { inf := fun (u₁ u₂ : ) => UniformSpace.mk () }
Equations
theorem iInf_uniformity {α : Type ua} {ι : Sort u_2} {u : ι} :
= ⨅ (i : ι),
theorem inf_uniformity {α : Type ua} {u : } {v : } :
=
theorem bot_uniformity {α : Type ua} :
theorem top_uniformity {α : Type ua} :
instance inhabitedUniformSpace {α : Type ua} :
Equations
• inhabitedUniformSpace = { default := }
instance inhabitedUniformSpaceCore {α : Type ua} :
Equations
• inhabitedUniformSpaceCore = { default := default.toCore }
Equations
• instUniqueUniformSpaceOfSubsingleton = { toInhabited := inhabitedUniformSpace, uniq := }
@[reducible, inline]
abbrev UniformSpace.comap {α : Type ua} {β : Type ub} (f : αβ) (u : ) :

Given f : α → β and a uniformity u on β, the inverse image of u under f is the inverse image in the filter sense of the induced function α × α → β × β. See note [reducible non-instances].

Equations
Instances For
theorem uniformity_comap {α : Type ua} {β : Type ub} :
∀ {x : } (f : αβ), = Filter.comap (Prod.map f f) ()
@[simp]
theorem uniformSpace_comap_id {α : Type u_2} :
= id
theorem UniformSpace.comap_comap {α : Type u_2} {β : Type u_3} {γ : Type u_4} {uγ : } {f : αβ} {g : βγ} :
theorem UniformSpace.comap_inf {α : Type u_2} {γ : Type u_3} {u₁ : } {u₂ : } {f : αγ} :
UniformSpace.comap f (u₁ u₂) =
theorem UniformSpace.comap_iInf {ι : Sort u_2} {α : Type u_3} {γ : Type u_4} {u : ι} {f : αγ} :
UniformSpace.comap f (⨅ (i : ι), u i) = ⨅ (i : ι), UniformSpace.comap f (u i)
theorem UniformSpace.comap_mono {α : Type u_2} {γ : Type u_3} {f : αγ} :
Monotone fun (u : ) =>
theorem uniformContinuous_iff {α : Type u_2} {β : Type u_3} {uα : } {uβ : } {f : αβ} :
theorem le_iff_uniformContinuous_id {α : Type ua} {u : } {v : } :
u v
theorem uniformContinuous_comap {α : Type ua} {β : Type ub} {f : αβ} [u : ] :
theorem uniformContinuous_comap' {α : Type ua} {β : Type ub} {γ : Type uc} {f : γβ} {g : αγ} [v : ] [u : ] (h : UniformContinuous (f g)) :
theorem UniformSpace.to_nhds_mono {α : Type ua} {u₁ : } {u₂ : } (h : u₁ u₂) (a : α) :
theorem UniformSpace.toTopologicalSpace_mono {α : Type ua} {u₁ : } {u₂ : } (h : u₁ u₂) :
UniformSpace.toTopologicalSpace UniformSpace.toTopologicalSpace
theorem UniformSpace.toTopologicalSpace_comap {α : Type ua} {β : Type ub} {f : αβ} {u : } :
UniformSpace.toTopologicalSpace = TopologicalSpace.induced f UniformSpace.toTopologicalSpace
theorem UniformSpace.uniformSpace_eq_bot {α : Type ua} {u : } :
u = idRel
theorem Filter.HasBasis.uniformSpace_eq_bot {α : Type ua} {ι : Sort u_2} {p : ιProp} {s : ιSet (α × α)} {u : } (h : ().HasBasis p s) :
u = ∃ (i : ι), p i Pairwise fun (x y : α) => (x, y)s i
theorem UniformSpace.toTopologicalSpace_bot {α : Type ua} :
UniformSpace.toTopologicalSpace =
theorem UniformSpace.toTopologicalSpace_top {α : Type ua} :
UniformSpace.toTopologicalSpace =
theorem UniformSpace.toTopologicalSpace_iInf {α : Type ua} {ι : Sort u_2} {u : ι} :
UniformSpace.toTopologicalSpace = ⨅ (i : ι), UniformSpace.toTopologicalSpace
theorem UniformSpace.toTopologicalSpace_sInf {α : Type ua} {s : Set ()} :
UniformSpace.toTopologicalSpace = is, UniformSpace.toTopologicalSpace
theorem UniformSpace.toTopologicalSpace_inf {α : Type ua} {u : } {v : } :
UniformSpace.toTopologicalSpace = UniformSpace.toTopologicalSpace UniformSpace.toTopologicalSpace
theorem UniformContinuous.continuous {α : Type ua} {β : Type ub} [] [] {f : αβ} (hf : ) :
instance ULift.uniformSpace {α : Type ua} [] :

Uniform space structure on ULift α.

Equations
theorem UniformContinuous.inf_rng {α : Type ua} {β : Type ub} {f : αβ} {u₁ : } {u₂ : } {u₃ : } (h₁ : ) (h₂ : ) :
theorem UniformContinuous.inf_dom_left {α : Type ua} {β : Type ub} {f : αβ} {u₁ : } {u₂ : } {u₃ : } (hf : ) :
theorem UniformContinuous.inf_dom_right {α : Type ua} {β : Type ub} {f : αβ} {u₁ : } {u₂ : } {u₃ : } (hf : ) :
theorem uniformContinuous_sInf_dom {α : Type ua} {β : Type ub} {f : αβ} {u₁ : Set ()} {u₂ : } {u : } (h₁ : u u₁) (hf : ) :
theorem uniformContinuous_sInf_rng {α : Type ua} {β : Type ub} {f : αβ} {u₁ : } {u₂ : Set ()} :
uu₂,
theorem uniformContinuous_iInf_dom {α : Type ua} {β : Type ub} {ι : Sort u_1} {f : αβ} {u₁ : ι} {u₂ : } {i : ι} (hf : ) :
theorem uniformContinuous_iInf_rng {α : Type ua} {β : Type ub} {ι : Sort u_1} {f : αβ} {u₁ : } {u₂ : ι} :
∀ (i : ι),
theorem discreteTopology_of_discrete_uniformity {α : Type ua} [hα : ] (h : = Filter.principal idRel) :

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

Equations
Equations
Equations
Equations
Equations
instance instUniformSpaceAdditive {α : Type ua} [] :
Equations
instance instUniformSpaceMultiplicative {α : Type ua} [] :
Equations
• instUniformSpaceMultiplicative = inst
theorem uniformContinuous_ofMul {α : Type ua} [] :
theorem uniformContinuous_toMul {α : Type ua} [] :
theorem uniformContinuous_ofAdd {α : Type ua} [] :
theorem uniformContinuous_toAdd {α : Type ua} [] :
theorem uniformity_additive {α : Type ua} [] :
theorem uniformity_multiplicative {α : Type ua} [] :
instance instUniformSpaceSubtype {α : Type ua} {p : αProp} [t : ] :
Equations
theorem uniformity_subtype {α : Type ua} {p : αProp} [] :
= Filter.comap (fun (q : × ) => (q.1, q.2)) ()
theorem uniformity_setCoe {α : Type ua} {s : Set α} [] :
= Filter.comap (Prod.map Subtype.val Subtype.val) ()
theorem map_uniformity_set_coe {α : Type ua} {s : Set α} [] :
Filter.map (Prod.map Subtype.val Subtype.val) () = Filter.principal (s ×ˢ s)
theorem uniformContinuous_subtype_val {α : Type ua} {p : αProp} [] :
UniformContinuous Subtype.val
theorem UniformContinuous.subtype_mk {α : Type ua} {β : Type ub} {p : αProp} [] [] {f : βα} (hf : ) (h : ∀ (x : β), p (f x)) :
UniformContinuous fun (x : β) => f x,
theorem uniformContinuousOn_iff_restrict {α : Type ua} {β : Type ub} [] [] {f : αβ} {s : Set α} :
UniformContinuous (s.restrict f)
theorem tendsto_of_uniformContinuous_subtype {α : Type ua} {β : Type ub} [] [] {f : αβ} {s : Set α} {a : α} (hf : UniformContinuous fun (x : s) => f x) (ha : s nhds a) :
Filter.Tendsto f (nhds a) (nhds (f a))
theorem UniformContinuousOn.continuousOn {α : Type ua} {β : Type ub} [] [] {f : αβ} {s : Set α} (h : ) :
instance instUniformSpaceAddOpposite {α : Type ua} [] :
Equations
instance instUniformSpaceMulOpposite {α : Type ua} [] :
Equations
theorem uniformity_addOpposite {α : Type ua} [] :
= Filter.comap (fun (q : αᵃᵒᵖ × αᵃᵒᵖ) => (, )) ()
theorem uniformity_mulOpposite {α : Type ua} [] :
= Filter.comap (fun (q : αᵐᵒᵖ × αᵐᵒᵖ) => (, )) ()
@[simp]
theorem comap_uniformity_addOpposite {α : Type ua} [] :
Filter.comap (fun (p : α × α) => (, )) () =
@[simp]
theorem comap_uniformity_mulOpposite {α : Type ua} [] :
Filter.comap (fun (p : α × α) => (, )) () =
theorem AddOpposite.uniformContinuous_unop {α : Type ua} [] :
theorem MulOpposite.uniformContinuous_unop {α : Type ua} [] :
UniformContinuous MulOpposite.unop
instance instUniformSpaceProd {α : Type ua} {β : Type ub} [u₁ : ] [u₂ : ] :
Equations
theorem uniformity_prod {α : Type ua} {β : Type ub} [] [] :
uniformity (α × β) = Filter.comap (fun (p : (α × β) × α × β) => (p.1.1, p.2.1)) () Filter.comap (fun (p : (α × β) × α × β) => (p.1.2, p.2.2)) ()
instance instIsCountablyGeneratedProdUniformity {α : Type ua} {β : Type ub} [] [().IsCountablyGenerated] [] [().IsCountablyGenerated] :
(uniformity (α × β)).IsCountablyGenerated
Equations
• =
theorem uniformity_prod_eq_comap_prod {α : Type ua} {β : Type ub} [] [] :
uniformity (α × β) = Filter.comap (fun (p : (α × β) × α × β) => ((p.1.1, p.2.1), p.1.2, p.2.2)) ()
theorem uniformity_prod_eq_prod {α : Type ua} {β : Type ub} [] [] :
uniformity (α × β) = Filter.map (fun (p : (α × α) × β × β) => ((p.1.1, p.2.1), p.1.2, p.2.2)) ()
theorem mem_uniformity_of_uniformContinuous_invariant {α : Type ua} {β : Type ub} [] [] {s : Set (β × β)} {f : ααβ} (hf : UniformContinuous fun (p : α × α) => f p.1 p.2) (hs : s ) :
u, ∀ (a b c : α), (a, b) u(f a c, f b c) s
theorem mem_uniform_prod {α : Type ua} {β : Type ub} [t₁ : ] [t₂ : ] {a : Set (α × α)} {b : Set (β × β)} (ha : a ) (hb : b ) :
{p : (α × β) × α × β | (p.1.1, p.2.1) a (p.1.2, p.2.2) b} uniformity (α × β)
theorem tendsto_prod_uniformity_fst {α : Type ua} {β : Type ub} [] [] :
Filter.Tendsto (fun (p : (α × β) × α × β) => (p.1.1, p.2.1)) (uniformity (α × β)) ()
theorem tendsto_prod_uniformity_snd {α : Type ua} {β : Type ub} [] [] :
Filter.Tendsto (fun (p : (α × β) × α × β) => (p.1.2, p.2.2)) (uniformity (α × β)) ()
theorem uniformContinuous_fst {α : Type ua} {β : Type ub} [] [] :
UniformContinuous fun (p : α × β) => p.1
theorem uniformContinuous_snd {α : Type ua} {β : Type ub} [] [] :
UniformContinuous fun (p : α × β) => p.2
theorem UniformContinuous.prod_mk {α : Type ua} {β : Type ub} {γ : Type uc} [] [] [] {f₁ : αβ} {f₂ : αγ} (h₁ : ) (h₂ : ) :
UniformContinuous fun (a : α) => (f₁ a, f₂ a)
theorem UniformContinuous.prod_mk_left {α : Type ua} {β : Type ub} {γ : Type uc} [] [] [] {f : α × βγ} (h : ) (b : β) :
UniformContinuous fun (a : α) => f (a, b)
theorem UniformContinuous.prod_mk_right {α : Type ua} {β : Type ub} {γ : Type uc} [] [] [] {f : α × βγ} (h : ) (a : α) :
UniformContinuous fun (b : β) => f (a, b)
theorem UniformContinuous.prod_map {α : Type ua} {β : Type ub} {γ : Type uc} {δ : Type ud} [] [] [] [] {f : αγ} {g : βδ} (hf : ) (hg : ) :
theorem toTopologicalSpace_prod {α : Type u_2} {β : Type u_3} [u : ] [v : ] :
UniformSpace.toTopologicalSpace = instTopologicalSpaceProd
theorem uniformContinuous_inf_dom_left₂ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : αβγ} {ua1 : } {ua2 : } {ub1 : } {ub2 : } {uc1 : } (h : UniformContinuous fun (p : α × β) => f p.1 p.2) :
UniformContinuous fun (p : α × β) => f p.1 p.2

A version of UniformContinuous.inf_dom_left for binary functions

theorem uniformContinuous_inf_dom_right₂ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : αβγ} {ua1 : } {ua2 : } {ub1 : } {ub2 : } {uc1 : } (h : UniformContinuous fun (p : α × β) => f p.1 p.2) :
UniformContinuous fun (p : α × β) => f p.1 p.2

A version of UniformContinuous.inf_dom_right for binary functions

theorem uniformContinuous_sInf_dom₂ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : αβγ} {uas : Set ()} {ubs : Set ()} {ua : } {ub : } {uc : } (ha : ua uas) (hb : ub ubs) (hf : UniformContinuous fun (p : α × β) => f p.1 p.2) :
UniformContinuous fun (p : α × β) => f p.1 p.2

A version of uniformContinuous_sInf_dom for binary functions

def UniformContinuous₂ {α : Type ua} {β : Type ub} {γ : Type uc} [] [] [] (f : αβγ) :

Uniform continuity for functions of two variables.

Equations
Instances For
theorem uniformContinuous₂_def {α : Type ua} {β : Type ub} {γ : Type uc} [] [] [] (f : αβγ) :
theorem UniformContinuous₂.uniformContinuous {α : Type ua} {β : Type ub} {γ : Type uc} [] [] [] {f : αβγ} (h : ) :
theorem uniformContinuous₂_curry {α : Type ua} {β : Type ub} {γ : Type uc} [] [] [] (f : α × βγ) :
theorem UniformContinuous₂.comp {α : Type ua} {β : Type ub} {γ : Type uc} {δ : Type ud} [] [] [] [] {f : αβγ} {g : γδ} (hg : ) (hf : ) :
theorem UniformContinuous₂.bicompl {α : Type ua} {β : Type ub} {γ : Type uc} {δ : Type ud} {δ' : Type u_2} [] [] [] [] [] {f : αβγ} {ga : δα} {gb : δ'β} (hf : ) (hga : ) (hgb : ) :
theorem toTopologicalSpace_subtype {α : Type ua} [u : ] {p : αProp} :
UniformSpace.toTopologicalSpace = instTopologicalSpaceSubtype
instance Sum.instUniformSpace {α : Type ua} {β : Type ub} [] [] :

Uniformity on a disjoint union. Entourages of the diagonal in the union are obtained by taking independently an entourage of the diagonal in the first part, and an entourage of the diagonal in the second part.

Equations
• One or more equations did not get rendered due to their size.
@[reducible, deprecated Sum.instUniformSpace]
def Sum.uniformSpace {α : Type ua} {β : Type ub} [] [] :

Alias of Sum.instUniformSpace.

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
Instances For
theorem union_mem_uniformity_sum {α : Type ua} {β : Type ub} [] [] {a : Set (α × α)} (ha : a ) {b : Set (β × β)} (hb : b ) :
Prod.map Sum.inl Sum.inl '' a Prod.map Sum.inr Sum.inr '' b uniformity (α β)

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

theorem Sum.uniformity {α : Type ua} {β : Type ub} [] [] :
uniformity (α β) = Filter.map (Prod.map Sum.inl Sum.inl) () Filter.map (Prod.map Sum.inr Sum.inr) ()
theorem uniformContinuous_inl {α : Type ua} {β : Type ub} [] [] :
theorem uniformContinuous_inr {α : Type ua} {β : Type ub} [] [] :
instance instIsCountablyGeneratedProdSumUniformity {α : Type ua} {β : Type ub} [] [] [().IsCountablyGenerated] [().IsCountablyGenerated] :
(uniformity (α β)).IsCountablyGenerated
Equations
• =

### Compact sets in uniform spaces #

theorem lebesgue_number_lemma {α : Type ua} [] {K : Set α} {ι : Sort u_2} {U : ιSet α} (hK : ) (hopen : ∀ (i : ι), IsOpen (U i)) (hcover : K ⋃ (i : ι), U i) :
V, xK, ∃ (i : ι), U 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 Filter.HasBasis.lebesgue_number_lemma {α : Type ua} [] {K : Set α} {ι' : Sort u_2} {ι : Sort u_3} {p : ι'Prop} {V : ι'Set (α × α)} {U : ιSet α} (hbasis : ().HasBasis p V) (hK : ) (hopen : ∀ (j : ι), IsOpen (U j)) (hcover : K ⋃ (j : ι), U j) :
∃ (i : ι'), p i xK, ∃ (j : ι), UniformSpace.ball x (V i) U j

Let U : ι → Set α be an open cover of a compact set K. Then there exists an entourage V such that for each x ∈ K its V-neighborhood is included in some U i.

Moreover, one can choose an entourage from a given basis.

theorem lebesgue_number_lemma_sUnion {α : Type ua} [] {K : Set α} {S : Set (Set α)} (hK : ) (hopen : sS, ) (hcover : K ⋃₀ S) :
V, xK, sS, s

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 IsCompact.nhdsSet_basis_uniformity {α : Type ua} {ι : Sort u_1} [] {K : Set α} {p : ιProp} {V : ιSet (α × α)} (hbasis : ().HasBasis p V) (hK : ) :
().HasBasis p fun (i : ι) => xK, UniformSpace.ball x (V i)

If K is a compact set in a uniform space and {V i | p i} is a basis of entourages, then {⋃ x ∈ K, UniformSpace.ball x (V i) | p i} is a basis of 𝓝ˢ K.

Here "{s i | p i} is a basis of a filter l" means Filter.HasBasis l p s.

theorem Disjoint.exists_uniform_thickening {α : Type ua} [] {A : Set α} {B : Set α} (hA : ) (hB : ) (h : Disjoint A B) :
V, Disjoint (xA, ) (xB, )
theorem Disjoint.exists_uniform_thickening_of_basis {α : Type ua} {ι : Sort u_1} [] {p : ιProp} {s : ιSet (α × α)} (hU : ().HasBasis p s) {A : Set α} {B : Set α} (hA : ) (hB : ) (h : Disjoint A B) :
∃ (i : ι), p i Disjoint (xA, UniformSpace.ball x (s i)) (xB, UniformSpace.ball x (s i))
theorem lebesgue_number_of_compact_open {α : Type ua} [] {K : Set α} {U : Set α} (hK : ) (hU : ) (hKU : K U) :
V, xK, 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 ua} {β : Type ub} [] {f : } {u : βα} {a : α} :
Filter.Tendsto u f (nhds a) Filter.Tendsto (fun (x : β) => (a, u x)) f ()
theorem Uniform.tendsto_nhds_left {α : Type ua} {β : Type ub} [] {f : } {u : βα} {a : α} :
Filter.Tendsto u f (nhds a) Filter.Tendsto (fun (x : β) => (u x, a)) f ()
theorem Uniform.continuousAt_iff'_right {α : Type ua} {β : Type ub} [] [] {f : βα} {b : β} :
Filter.Tendsto (fun (x : β) => (f b, f x)) (nhds b) ()
theorem Uniform.continuousAt_iff'_left {α : Type ua} {β : Type ub} [] [] {f : βα} {b : β} :
Filter.Tendsto (fun (x : β) => (f x, f b)) (nhds b) ()
theorem Uniform.continuousAt_iff_prod {α : Type ua} {β : Type ub} [] [] {f : βα} {b : β} :
Filter.Tendsto (fun (x : β × β) => (f x.1, f x.2)) (nhds (b, b)) ()
theorem Uniform.continuousWithinAt_iff'_right {α : Type ua} {β : Type ub} [] [] {f : βα} {b : β} {s : Set β} :
Filter.Tendsto (fun (x : β) => (f b, f x)) () ()
theorem Uniform.continuousWithinAt_iff'_left {α : Type ua} {β : Type ub} [] [] {f : βα} {b : β} {s : Set β} :
Filter.Tendsto (fun (x : β) => (f x, f b)) () ()
theorem Uniform.continuousOn_iff'_right {α : Type ua} {β : Type ub} [] [] {f : βα} {s : Set β} :
bs, Filter.Tendsto (fun (x : β) => (f b, f x)) () ()
theorem Uniform.continuousOn_iff'_left {α : Type ua} {β : Type ub} [] [] {f : βα} {s : Set β} :
bs, Filter.Tendsto (fun (x : β) => (f x, f b)) () ()
theorem Uniform.continuous_iff'_right {α : Type ua} {β : Type ub} [] [] {f : βα} :
∀ (b : β), Filter.Tendsto (fun (x : β) => (f b, f x)) (nhds b) ()
theorem Uniform.continuous_iff'_left {α : Type ua} {β : Type ub} [] [] {f : βα} :
∀ (b : β), Filter.Tendsto (fun (x : β) => (f x, f b)) (nhds b) ()
theorem Uniform.exists_is_open_mem_uniformity_of_forall_mem_eq {α : Type ua} {β : Type ub} [] [] {r : Set (α × α)} {s : Set β} {f : βα} {g : βα} (hf : xs, ) (hg : xs, ) (hfg : Set.EqOn f g s) (hr : r ) :
∃ (t : Set β), s t xt, (f x, g x) r

Consider two functions f and g which coincide on a set s and are continuous there. Then there is an open neighborhood of s on which f and g are uniformly close.

theorem Filter.Tendsto.congr_uniformity {α : Type u_2} {β : Type u_3} [] {f : αβ} {g : αβ} {l : } {b : β} (hf : Filter.Tendsto f l (nhds b)) (hg : Filter.Tendsto (fun (x : α) => (f x, g x)) l ()) :
theorem Uniform.tendsto_congr {α : Type u_2} {β : Type u_3} [] {f : αβ} {g : αβ} {l : } {b : β} (hfg : Filter.Tendsto (fun (x : α) => (f x, g x)) l ()) :