Uniform spaces #
Uniform spaces are a generalization of metric spaces and topological groups. Many concepts directly generalize to uniform spaces, e.g.
- uniform continuity (in this file)
- completeness (in
Cauchy.lean
) - extension of uniform continuous functions to complete spaces (in
IsUniformEmbedding.lean
) - totally bounded sets (in
Cauchy.lean
) - totally bounded complete sets are compact (in
Cauchy.lean
)
A uniform structure on a type X
is a filter 𝓤 X
on X × X
satisfying some conditions
which makes it reasonable to say that ∀ᶠ (p : X × X) in 𝓤 X, ...
means
"for all p.1 and p.2 in X close enough, ...". Elements of this filter are called entourages
of X
. The two main examples are:
- If
X
is a metric space,V ∈ 𝓤 X ↔ ∃ ε > 0, { p | dist p.1 p.2 < ε } ⊆ V
- If
G
is an additive topological group,V ∈ 𝓤 G ↔ ∃ U ∈ 𝓝 (0 : G), {p | p.2 - p.1 ∈ U} ⊆ V
Those examples are generalizations in two different directions of the elementary example where
X = ℝ
and V ∈ 𝓤 ℝ ↔ ∃ ε > 0, { p | |p.2 - p.1| < ε } ⊆ V
which features both the topological
group structure on ℝ
and its metric space structure.
Each uniform structure on X
induces a topology on X
characterized by
nhds_eq_comap_uniformity : ∀ {x : X}, 𝓝 x = comap (Prod.mk x) (𝓤 X)
where Prod.mk x : X → X × X := (fun y ↦ (x, y))
is the partial evaluation of the product
constructor.
The dictionary with metric spaces includes:
- an upper bound for
dist x y
translates into(x, y) ∈ V
for someV ∈ 𝓤 X
- a ball
ball x r
roughly corresponds toUniformSpace.ball x V := {y | (x, y) ∈ V}
for someV ∈ 𝓤 X
, but the later is more general (it includes in particular both open and closed balls for suitableV
). 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 diagonalidRel = { p | p.1 = p.2 }
. This abstracts the fact thatdist x x ≤ r
for every non-negative radiusr
in the metric space case and also thatx - x
belongs to every neighborhood of zero in the topological group case. V ∈ 𝓤 X → Prod.swap '' V ∈ 𝓤 X
. This is tightly related the fact thatdist 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 typeX
UniformContinuous f
is a predicate saying a functionf : α → β
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:
- [N. Bourbaki, General Topology][bourbaki1966]
- [I. M. James, Topologies and Uniformities][james1999]
But it makes a more systematic use of the filter library.
The composition of relations
Equations
- Uniformity.«term_○_» = Lean.ParserDescr.trailingNode `Uniformity.term_○_ 62 62 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ○ ") (Lean.ParserDescr.cat `term 63))
Instances For
The relation is invariant under swapping factors.
Equations
- SymmetricRel V = (Prod.swap ⁻¹' V = V)
Instances For
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.
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
, thenProd.swap ⁻¹' s ∈ uniformity
. For every set
u ∈ uniformity
, there existsv ∈ uniformity
such thatv ○ v ⊆ u
.
Instances For
Every set in the uniformity filter includes the diagonal.
If s ∈ uniformity
, then Prod.swap ⁻¹' s ∈ uniformity
.
For every set u ∈ uniformity
, there exists v ∈ uniformity
such that v ○ v ⊆ u
.
An alternative constructor for UniformSpace.Core
. This version unfolds various
Filter
-related definitions.
Equations
- UniformSpace.Core.mk' U refl symm comp = { uniformity := U, refl := ⋯, symm := symm, comp := ⋯ }
Instances For
Defining a UniformSpace.Core
from a filter basis satisfying some uniformity-like axioms.
Equations
- UniformSpace.Core.mkOfBasis B refl symm comp = { uniformity := B.filter, refl := ⋯, symm := ⋯, comp := ⋯ }
Instances For
A uniform space generates a topological space
Equations
- u.toTopologicalSpace = TopologicalSpace.mkOfNhds fun (x : α) => Filter.comap (Prod.mk x) u.uniformity
Instances For
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_univ : TopologicalSpace.IsOpen Set.univ
- isOpen_inter : ∀ (s t : Set α), TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
- isOpen_sUnion : ∀ (s : Set (Set α)), (∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
The uniformity filter.
- symm : Filter.Tendsto Prod.swap UniformSpace.uniformity UniformSpace.uniformity
If
s ∈ uniformity
, thenProd.swap ⁻¹' s ∈ uniformity
. - comp : (UniformSpace.uniformity.lift' fun (s : Set (α × α)) => compRel s s) ≤ UniformSpace.uniformity
For every set
u ∈ uniformity
, there existsv ∈ uniformity
such thatv ○ v ⊆ u
. - nhds_eq_comap_uniformity : ∀ (x : α), nhds x = Filter.comap (Prod.mk x) UniformSpace.uniformity
The uniformity agrees with the topology: the neighborhoods filter of each point
x
is equal toFilter.comap (Prod.mk x) (𝓤 α)
.
Instances
If s ∈ uniformity
, then Prod.swap ⁻¹' s ∈ uniformity
.
For every set u ∈ uniformity
, there exists v ∈ uniformity
such that v ○ v ⊆ u
.
The uniformity agrees with the topology: the neighborhoods filter of each point x
is equal to Filter.comap (Prod.mk x) (𝓤 α)
.
The uniformity is a filter on α × α (inferred from an ambient uniform space structure on α).
Equations
- uniformity α = 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
- Uniformity.term𝓤 = Lean.ParserDescr.node `Uniformity.term𝓤 1024 (Lean.ParserDescr.symbol "𝓤")
Instances For
Construct a UniformSpace
from a u : UniformSpace.Core
and a TopologicalSpace
structure
that is equal to u.toTopologicalSpace
.
Equations
- UniformSpace.ofCoreEq u t h = UniformSpace.mk u.uniformity ⋯ ⋯ ⋯
Instances For
Construct a UniformSpace
from a UniformSpace.Core
.
Equations
- UniformSpace.ofCore u = UniformSpace.ofCoreEq u u.toTopologicalSpace ⋯
Instances For
Construct a UniformSpace.Core
from a UniformSpace
.
Equations
- u.toCore = { uniformity := UniformSpace.uniformity, refl := ⋯, symm := ⋯, comp := ⋯ }
Instances For
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
- UniformSpace.ofNhdsEqComap u _t h = UniformSpace.mk u.uniformity ⋯ ⋯ h
Instances For
Replace topology in a UniformSpace
instance with a propositionally (but possibly not
definitionally) equal one.
Equations
- u.replaceTopology h = UniformSpace.mk UniformSpace.uniformity ⋯ ⋯ ⋯
Instances For
Equations
- ⋯ = ⋯
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).
If s ∈ 𝓤 α
, then for a subset t
of a sufficiently small set in 𝓤 α
,
we have t ○ t ⊆ s
.
Relation fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)
is transitive.
Relation fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)
is symmetric.
Relation fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)
is reflexive.
Symmetric entourages form a basis of 𝓤 α
See also comp3_mem_uniformity
.
See also comp_open_symm_mem_uniformity_sets
.
Balls in uniform spaces #
The ball around (x : β)
with respect to (V : Set (β × β))
. Intended to be
used for V ∈ 𝓤 β
, but this is not needed for the definition. Recovers the
notions of metric space ball when V = {p | dist p.1 p.2 < r }
.
Equations
- UniformSpace.ball x V = Prod.mk x ⁻¹' V
Instances For
The triangle inequality for UniformSpace.ball
Neighborhoods in uniform spaces #
See also isOpen_iff_open_ball_subset
.
Entourages are neighborhoods of the diagonal.
Entourages are neighborhoods of the diagonal.
Entourages are neighborhoods of the diagonal.
Closure and interior in uniform spaces #
Closed entourages form a basis of the uniformity filter.
The uniform neighborhoods of all points of a dense set cover the whole space.
The uniform neighborhoods of all points of a dense indexed collection cover the whole space.
Uniformity bases #
Open elements of 𝓤 α
form a basis of 𝓤 α
.
Open elements s : Set (α × α)
of 𝓤 α
such that (x, y) ∈ s ↔ (y, x) ∈ s
form a basis
of 𝓤 α
.
Uniform continuity #
A function f : α → β
is uniformly continuous if (f x, f y)
tends to the diagonal
as (x, y)
tends to the diagonal. In other words, if x
is sufficiently close to y
, then
f x
is close to f y
no matter where x
and y
are located in α
.
Equations
- UniformContinuous f = Filter.Tendsto (fun (x : α × α) => (f x.1, f x.2)) (uniformity α) (uniformity β)
Instances For
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
A function f : α → β
is uniformly continuous on s : Set α
if (f x, f y)
tends to
the diagonal as (x, y)
tends to the diagonal while remaining in s ×ˢ s
.
In other words, if x
is sufficiently close to y
, then f x
is close to
f y
no matter where x
and y
are located in s
.
Equations
- UniformContinuousOn f s = Filter.Tendsto (fun (x : α × α) => (f x.1, f x.2)) (uniformity α ⊓ Filter.principal (s ×ˢ s)) (uniformity β)
Instances For
If a function T
is uniformly continuous in a uniform space β
,
then its n
-th iterate T^[n]
is also uniformly continuous.
Equations
- instPartialOrderUniformSpace = PartialOrder.lift (fun (u : UniformSpace α) => uniformity α) ⋯
Equations
- instInfSetUniformSpace = { sInf := fun (s : Set (UniformSpace α)) => UniformSpace.ofCore { uniformity := ⨅ u ∈ s, uniformity α, refl := ⋯, symm := ⋯, comp := ⋯ } }
Equations
- instTopUniformSpace = { top := UniformSpace.mk ⊤ ⋯ ⋯ ⋯ }
Equations
- instBotUniformSpace = { bot := UniformSpace.mk (Filter.principal idRel) ⋯ ⋯ ⋯ }
Equations
- instInfUniformSpace = { inf := fun (u₁ u₂ : UniformSpace α) => UniformSpace.mk (uniformity α ⊓ uniformity α) ⋯ ⋯ ⋯ }
Equations
- instCompleteLatticeUniformSpace = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- inhabitedUniformSpaceCore = { default := default.toCore }
Equations
- instUniqueUniformSpaceOfSubsingleton = { toInhabited := inhabitedUniformSpace, uniq := ⋯ }
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
- UniformSpace.comap f u = UniformSpace.mk (Filter.comap (fun (p : α × α) => (f p.1, f p.2)) (uniformity β)) ⋯ ⋯ ⋯
Instances For
Uniform space structure on ULift α
.
Equations
- ULift.uniformSpace = UniformSpace.comap ULift.down inst
A uniform space with the discrete uniformity has the discrete topology.
Equations
Equations
- instUniformSpaceAdditive = inst
Equations
- instUniformSpaceMultiplicative = inst
Equations
- instUniformSpaceSubtype = UniformSpace.comap Subtype.val t
Equations
- instUniformSpaceAddOpposite = UniformSpace.comap AddOpposite.unop inst
Equations
- instUniformSpaceMulOpposite = UniformSpace.comap MulOpposite.unop inst
Equations
- instUniformSpaceProd = UniformSpace.comap Prod.fst u₁ ⊓ UniformSpace.comap Prod.snd u₂
Equations
- ⋯ = ⋯
A version of UniformContinuous.inf_dom_left
for binary functions
A version of UniformContinuous.inf_dom_right
for binary functions
A version of uniformContinuous_sInf_dom
for binary functions
Uniform continuity for functions of two variables.
Equations
Instances For
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.
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
The union of an entourage of the diagonal in each set of a disjoint union is again an entourage of the diagonal.
Equations
- ⋯ = ⋯
Compact sets in uniform spaces #
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
.
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.
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
.
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
.
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.
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.