Topology and uniform structure of uniform convergence #
This files endows α → β
with the topologies / uniform structures of
- uniform convergence on
α
- uniform convergence on a specified family
𝔖
of sets ofα
, also called𝔖
-convergence
Since α → β
is already endowed with the topologies and uniform structures of pointwise
convergence, we introduce type aliases UniformFun α β
(denoted α →ᵤ β
) and
UniformOnFun α β 𝔖
(denoted α →ᵤ[𝔖] β
) and we actually endow these with the structures
of uniform and 𝔖
-convergence respectively.
Usual examples of the second construction include :
- the topology of compact convergence, when
𝔖
is the set of compacts ofα
- the strong topology on the dual of a topological vector space (TVS)
E
, when𝔖
is the set of Von Neumann bounded subsets ofE
- the weak-* topology on the dual of a TVS
E
, when𝔖
is the set of singletons ofE
.
This file contains a lot of technical facts, so it is heavily commented, proofs included!
Main definitions #
UniformFun.gen
: basis sets for the uniformity of uniform convergence. These are sets of the formS(V) := {(f, g) | ∀ x : α, (f x, g x) ∈ V}
for someV : Set (β × β)
UniformFun.uniformSpace
: uniform structure of uniform convergence. This is theUniformSpace
onα →ᵤ β
whose uniformity is generated by the setsS(V)
forV ∈ 𝓤 β
. We will denote this uniform space as𝒰(α, β, uβ)
, both in the comments and as a local notation in the Lean code, whereuβ
is the uniform space structure onβ
. This is declared as an instance onα →ᵤ β
.UniformOnFun.uniformSpace
: uniform structure of𝔖
-convergence, where𝔖 : Set (Set α)
. This is the infimum, forS ∈ 𝔖
, of the pullback of𝒰 S β
by the map of restriction toS
. We will denote it𝒱(α, β, 𝔖, uβ)
, whereuβ
is the uniform space structure onβ
. This is declared as an instance onα →ᵤ[𝔖] β
.
Main statements #
Basic properties #
UniformFun.uniformContinuous_eval
: evaluation is uniformly continuous onα →ᵤ β
.UniformFun.t2Space
: the topology of uniform convergence onα →ᵤ β
is T₂ ifβ
is T₂.UniformFun.tendsto_iff_tendstoUniformly
:𝒰(α, β, uβ)
is indeed the uniform structure of uniform convergenceUniformOnFun.uniformContinuous_eval_of_mem
: evaluation at a point contained in a set of𝔖
is uniformly continuous onα →ᵤ[𝔖] β
UniformOnFun.t2Space_of_covering
: the topology of𝔖
-convergence onα →ᵤ[𝔖] β
is T₂ ifβ
is T₂ and𝔖
coversα
UniformOnFun.tendsto_iff_tendstoUniformlyOn
:𝒱(α, β, 𝔖 uβ)
is indeed the uniform structure of𝔖
-convergence
Functoriality and compatibility with product of uniform spaces #
In order to avoid the need for filter bases as much as possible when using these definitions,
we develop an extensive API for manipulating these structures abstractly. As usual in the topology
section of mathlib, we first state results about the complete lattices of UniformSpace
s on
fixed types, and then we use these to deduce categorical-like results about maps between two
uniform spaces.
We only describe these in the harder case of 𝔖
-convergence, as the names of the corresponding
results for uniform convergence can easily be guessed.
Order statements #
UniformOnFun.mono
: letu₁
,u₂
be two uniform structures onγ
and𝔖₁ 𝔖₂ : Set (Set α)
. Ifu₁ ≤ u₂
and𝔖₂ ⊆ 𝔖₁
then𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂)
.UniformOnFun.iInf_eq
: ifu
is a family of uniform structures onγ
, then𝒱(α, γ, 𝔖, (⨅ i, u i)) = ⨅ i, 𝒱(α, γ, 𝔖, u i)
.UniformOnFun.comap_eq
: ifu
is a uniform structures onβ
andf : γ → β
, then𝒱(α, γ, 𝔖, comap f u) = comap (fun g ↦ f ∘ g) 𝒱(α, γ, 𝔖, u₁)
.
An interesting note about these statements is that they are proved without ever unfolding the basis
definition of the uniform structure of uniform convergence! Instead, we build a
(not very interesting) Galois connection UniformFun.gc
and then rely on the Galois
connection API to do most of the work.
Morphism statements (unbundled) #
UniformOnFun.postcomp_uniformContinuous
: iff : γ → β
is uniformly continuous, then(fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β)
is uniformly continuous.UniformOnFun.postcomp_uniformInducing
: iff : γ → β
is a uniform inducing, then(fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β)
is a uniform inducing.UniformOnFun.precomp_uniformContinuous
: letf : γ → α
,𝔖 : Set (Set α)
,𝔗 : Set (Set γ)
, and assume that∀ T ∈ 𝔗, f '' T ∈ 𝔖
. Then, the function(fun g ↦ g ∘ f) : (α →ᵤ[𝔖] β) → (γ →ᵤ[𝔗] β)
is uniformly continuous.
Isomorphism statements (bundled) #
UniformOnFun.congrRight
: turn a uniform isomorphismγ ≃ᵤ β
into a uniform isomorphism(α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β)
by post-composing.UniformOnFun.congrLeft
: turn a bijectione : γ ≃ α
such that we have both∀ T ∈ 𝔗, e '' T ∈ 𝔖
and∀ S ∈ 𝔖, e ⁻¹' S ∈ 𝔗
into a uniform isomorphism(γ →ᵤ[𝔗] β) ≃ᵤ (α →ᵤ[𝔖] β)
by pre-composing.UniformOnFun.uniformEquivPiComm
: the natural bijection betweenα → Π i, δ i
andΠ i, α → δ i
, upgraded to a uniform isomorphism betweenα →ᵤ[𝔖] (Π i, δ i)
andΠ i, α →ᵤ[𝔖] δ i
.
Important use cases #
- If
G
is a uniform group, thenα →ᵤ[𝔖] G
is a uniform group: since(/) : G × G → G
is uniformly continuous,UniformOnFun.postcomp_uniformContinuous
tells us that((/) ∘ —) : (α →ᵤ[𝔖] G × G) → (α →ᵤ[𝔖] G)
is uniformly continuous. By precomposing withUniformOnFun.uniformEquivProdArrow
, this gives that(/) : (α →ᵤ[𝔖] G) × (α →ᵤ[𝔖] G) → (α →ᵤ[𝔖] G)
is also uniformly continuous - The transpose of a continuous linear map is continuous for the strong topologies: since
continuous linear maps are uniformly continuous and map bounded sets to bounded sets,
this is just a special case of
UniformOnFun.precomp_uniformContinuous
.
TODO #
- Show that the uniform structure of
𝔖
-convergence is exactly the structure of𝔖'
-convergence, where𝔖'
is the noncovering bornology (i.e not whatBornology
currently refers to in mathlib) generated by𝔖
.
References #
- [N. Bourbaki, General Topology, Chapter X][bourbaki1966]
Tags #
uniform convergence
The type of functions from α
to β
equipped with the uniform structure and topology of
uniform convergence. We denote it α →ᵤ β
.
Equations
- UniformFun α β = (α → β)
Instances For
The type of functions from α
to β
equipped with the uniform structure and topology of
uniform convergence on some family 𝔖
of subsets of α
. We denote it α →ᵤ[𝔖] β
.
Equations
- UniformOnFun α β x = (α → β)
Instances For
The type of functions from α
to β
equipped with the uniform structure and topology of
uniform convergence. We denote it α →ᵤ β
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The type of functions from α
to β
equipped with the uniform structure and topology of
uniform convergence on some family 𝔖
of subsets of α
. We denote it α →ᵤ[𝔖] β
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Reinterpret f : α → β
as an element of α →ᵤ β
.
Equations
- UniformFun.ofFun = { toFun := fun (x : α → β) => x, invFun := fun (x : UniformFun α β) => x, left_inv := ⋯, right_inv := ⋯ }
Instances For
Reinterpret f : α → β
as an element of α →ᵤ[𝔖] β
.
Equations
- UniformOnFun.ofFun 𝔖 = { toFun := fun (x : α → β) => x, invFun := fun (x : UniformOnFun α β 𝔖) => x, left_inv := ⋯, right_inv := ⋯ }
Instances For
Reinterpret f : α →ᵤ β
as an element of α → β
.
Equations
- UniformFun.toFun = UniformFun.ofFun.symm
Instances For
Reinterpret f : α →ᵤ[𝔖] β
as an element of α → β
.
Equations
- UniformOnFun.toFun 𝔖 = (UniformOnFun.ofFun 𝔖).symm
Instances For
Basis sets for the uniformity of uniform convergence: gen α β V
is the set of pairs (f, g)
of functions α →ᵤ β
such that ∀ x, (f x, g x) ∈ V
.
Equations
- UniformFun.gen α β V = {uv : UniformFun α β × UniformFun α β | ∀ (x : α), (UniformFun.toFun uv.1 x, UniformFun.toFun uv.2 x) ∈ V}
Instances For
If 𝓕
is a filter on β × β
, then the set of all UniformFun.gen α β V
for
V ∈ 𝓕
is a filter basis on (α →ᵤ β) × (α →ᵤ β)
. This will only be applied to 𝓕 = 𝓤 β
when
β
is equipped with a UniformSpace
structure, but it is useful to define it for any filter in
order to be able to state that it has a lower adjoint (see UniformFun.gc
).
For 𝓕 : Filter (β × β)
, this is the set of all UniformFun.gen α β V
for
V ∈ 𝓕
as a bundled FilterBasis
over (α →ᵤ β) × (α →ᵤ β)
. This will only be applied to
𝓕 = 𝓤 β
when β
is equipped with a UniformSpace
structure, but it is useful to define it for
any filter in order to be able to state that it has a lower adjoint
(see UniformFun.gc
).
Equations
- UniformFun.basis α β 𝓕 = ⋯.filterBasis
Instances For
For 𝓕 : Filter (β × β)
, this is the filter generated by the filter basis
UniformFun.basis α β 𝓕
. For 𝓕 = 𝓤 β
, this will be the uniformity of uniform
convergence on α
.
Equations
- UniformFun.filter α β 𝓕 = (UniformFun.basis α β 𝓕).filter
Instances For
Equations
- UniformFun.phi α β uvx = (uvx.1.1 uvx.2, uvx.1.2 uvx.2)
Instances For
The function UniformFun.filter α β : Filter (β × β) → Filter ((α →ᵤ β) × (α →ᵤ β))
has a lower adjoint l
(in the sense of GaloisConnection
). The exact definition of l
is not
interesting; we will only use that it exists (in UniformFun.mono
and
UniformFun.iInf_eq
) and that
l (Filter.map (Prod.map f f) 𝓕) = Filter.map (Prod.map ((∘) f) ((∘) f)) (l 𝓕)
for each
𝓕 : Filter (γ × γ)
and f : γ → α
(in UniformFun.comap_eq
).
Core of the uniform structure of uniform convergence.
Equations
- UniformFun.uniformCore α β = UniformSpace.Core.mkOfBasis (UniformFun.basis α β (uniformity β)) ⋯ ⋯ ⋯
Instances For
Uniform structure of uniform convergence, declared as an instance on α →ᵤ β
.
We will denote it 𝒰(α, β, uβ)
in the rest of this file.
Equations
Topology of uniform convergence, declared as an instance on α →ᵤ β
.
Equations
- UniformFun.topologicalSpace α β = inferInstance
By definition, the uniformity of α →ᵤ β
admits the family {(f, g) | ∀ x, (f x, g x) ∈ V}
for V ∈ 𝓤 β
as a filter basis.
The uniformity of α →ᵤ β
admits the family {(f, g) | ∀ x, (f x, g x) ∈ V}
for V ∈ 𝓑
as
a filter basis, for any basis 𝓑
of 𝓤 β
(in the case 𝓑 = (𝓤 β).as_basis
this is true by
definition).
For f : α →ᵤ β
, 𝓝 f
admits the family {g | ∀ x, (f x, g x) ∈ V}
for V ∈ 𝓑
as a filter
basis, for any basis 𝓑
of 𝓤 β
.
For f : α →ᵤ β
, 𝓝 f
admits the family {g | ∀ x, (f x, g x) ∈ V}
for V ∈ 𝓤 β
as a
filter basis.
Evaluation at a fixed point is uniformly continuous on α →ᵤ β
.
If u₁
and u₂
are two uniform structures on γ
and u₁ ≤ u₂
, then
𝒰(α, γ, u₁) ≤ 𝒰(α, γ, u₂)
.
If u
is a family of uniform structures on γ
, then
𝒰(α, γ, (⨅ i, u i)) = ⨅ i, 𝒰(α, γ, u i)
.
If u₁
and u₂
are two uniform structures on γ
, then
𝒰(α, γ, u₁ ⊓ u₂) = 𝒰(α, γ, u₁) ⊓ 𝒰(α, γ, u₂)
.
Post-composition by a uniform inducing function is a uniform inducing function for the uniform structures of uniform convergence.
More precisely, if f : γ → β
is uniform inducing,
then (f ∘ ·) : (α →ᵤ γ) → (α →ᵤ β)
is uniform inducing.
Post-composition by a uniform embedding is a uniform embedding for the uniform structures of uniform convergence.
More precisely, if f : γ → β
is a uniform embedding,
then (f ∘ ·) : (α →ᵤ γ) → (α →ᵤ β)
is a uniform embedding.
Alias of UniformFun.postcomp_isUniformEmbedding
.
Post-composition by a uniform embedding is a uniform embedding for the uniform structures of uniform convergence.
More precisely, if f : γ → β
is a uniform embedding,
then (f ∘ ·) : (α →ᵤ γ) → (α →ᵤ β)
is a uniform embedding.
If u
is a uniform structures on β
and f : γ → β
, then
𝒰(α, γ, comap f u) = comap (fun g ↦ f ∘ g) 𝒰(α, γ, u₁)
.
Post-composition by a uniformly continuous function is uniformly continuous on α →ᵤ β
.
More precisely, if f : γ → β
is uniformly continuous, then (fun g ↦ f ∘ g) : (α →ᵤ γ) → (α →ᵤ β)
is uniformly continuous.
Turn a uniform isomorphism γ ≃ᵤ β
into a uniform isomorphism (α →ᵤ γ) ≃ᵤ (α →ᵤ β)
by
post-composing.
Equations
- UniformFun.congrRight e = { toEquiv := Equiv.piCongrRight fun (x : α) => e.toEquiv, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
Instances For
Pre-composition by any function is uniformly continuous for the uniform structures of uniform convergence.
More precisely, for any f : γ → α
, the function (· ∘ f) : (α →ᵤ β) → (γ →ᵤ β)
is uniformly
continuous.
Turn a bijection γ ≃ α
into a uniform isomorphism
(γ →ᵤ β) ≃ᵤ (α →ᵤ β)
by pre-composing.
Equations
- UniformFun.congrLeft e = { toEquiv := e.arrowCongr (Equiv.refl β), uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
Instances For
The natural map UniformFun.toFun
from α →ᵤ β
to α → β
is uniformly continuous.
In other words, the uniform structure of uniform convergence is finer than that of pointwise convergence, aka the product uniform structure.
The topology of uniform convergence is T₂.
Equations
- ⋯ = ⋯
The topology of uniform convergence indeed gives the same notion of convergence as
TendstoUniformly
.
The natural bijection between α → β × γ
and (α → β) × (α → γ)
, upgraded to a uniform
isomorphism between α →ᵤ β × γ
and (α →ᵤ β) × (α →ᵤ γ)
.
Equations
- UniformFun.uniformEquivProdArrow = (Equiv.arrowProdEquivProdArrow β γ α).toUniformEquivOfUniformInducing ⋯
Instances For
The natural bijection between α → Π i, δ i
and Π i, α → δ i
, upgraded to a uniform
isomorphism between α →ᵤ (Π i, δ i)
and Π i, α →ᵤ δ i
.
Equations
- UniformFun.uniformEquivPiComm α δ = (Equiv.piComm fun (a : α) => δ).toUniformEquivOfUniformInducing ⋯
Instances For
The set of continuous functions is closed in the uniform convergence topology.
This is a simple wrapper over TendstoUniformly.continuous
.
Basis sets for the uniformity of 𝔖
-convergence: for S : Set α
and V : Set (β × β)
,
gen 𝔖 S V
is the set of pairs (f, g)
of functions α →ᵤ[𝔖] β
such that
∀ x ∈ S, (f x, g x) ∈ V
. Note that the family 𝔖 : Set (Set α)
is only used to specify which
type alias of α → β
to use here.
Equations
- UniformOnFun.gen 𝔖 S V = {uv : UniformOnFun α β 𝔖 × UniformOnFun α β 𝔖 | ∀ x ∈ S, ((UniformOnFun.toFun 𝔖) uv.1 x, (UniformOnFun.toFun 𝔖) uv.2 x) ∈ V}
Instances For
For S : Set α
and V : Set (β × β)
, we have
UniformOnFun.gen 𝔖 S V = (S.restrict × S.restrict) ⁻¹' (UniformFun.gen S β V)
.
This is the crucial fact for proving that the family UniformOnFun.gen S V
for S ∈ 𝔖
and
V ∈ 𝓤 β
is indeed a basis for the uniformity α →ᵤ[𝔖] β
endowed with 𝒱(α, β, 𝔖, uβ)
the uniform structure of 𝔖
-convergence, as defined in UniformOnFun.uniformSpace
.
UniformOnFun.gen
is antitone in the first argument and monotone in the second.
If 𝔖 : Set (Set α)
is nonempty and directed and 𝓑
is a filter basis on β × β
, then the
family UniformOnFun.gen 𝔖 S V
for S ∈ 𝔖
and V ∈ 𝓑
is a filter basis on
(α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)
.
We will show in has_basis_uniformity_of_basis
that, if 𝓑
is a basis for 𝓤 β
, then the
corresponding filter is the uniformity of α →ᵤ[𝔖] β
.
Uniform structure of 𝔖
-convergence, i.e uniform convergence on the elements of 𝔖
,
declared as an instance on α →ᵤ[𝔖] β
. It is defined as the infimum, for S ∈ 𝔖
, of the pullback
by S.restrict
, the map of restriction to S
, of the uniform structure 𝒰(s, β, uβ)
on
↥S →ᵤ β
. We will denote it 𝒱(α, β, 𝔖, uβ)
, where uβ
is the uniform structure on β
.
Equations
- UniformOnFun.uniformSpace α β 𝔖 = ⨅ s ∈ 𝔖, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) (UniformFun.uniformSpace (↑s) β)
Topology of 𝔖
-convergence, i.e uniform convergence on the elements of 𝔖
, declared as an
instance on α →ᵤ[𝔖] β
.
Equations
- UniformOnFun.topologicalSpace α β 𝔖 = UniformSpace.toTopologicalSpace
The topology of 𝔖
-convergence is the infimum, for S ∈ 𝔖
, of topology induced by the map
of S.restrict : (α →ᵤ[𝔖] β) → (↥S →ᵤ β)
of restriction to S
, where ↥S →ᵤ β
is endowed with
the topology of uniform convergence.
If 𝔖 : Set (Set α)
is nonempty and directed and 𝓑
is a filter basis of 𝓤 β
, then the
uniformity of α →ᵤ[𝔖] β
admits the family {(f, g) | ∀ x ∈ S, (f x, g x) ∈ V}
for S ∈ 𝔖
and
V ∈ 𝓑
as a filter basis.
If 𝔖 : Set (Set α)
is nonempty and directed, then the uniformity of α →ᵤ[𝔖] β
admits the
family {(f, g) | ∀ x ∈ S, (f x, g x) ∈ V}
for S ∈ 𝔖
and V ∈ 𝓤 β
as a filter basis.
Let t i
be a nonempty directed subfamily of 𝔖
such that every s ∈ 𝔖
is included in some t i
.
Let V
bounded by p
be a basis of entourages of β
.
Then UniformOnFun.gen 𝔖 (t i) (V j)
bounded by p j
is a basis of entourages of α →ᵤ[𝔖] β
.
If t n
is a monotone sequence of sets in 𝔖
such that each s ∈ 𝔖
is included in some t n
and V n
is an antitone basis of entourages of β
,
then UniformOnFun.gen 𝔖 (t n) (V n)
is an antitone basis of entourages of α →ᵤ[𝔖] β
.
For f : α →ᵤ[𝔖] β
, where 𝔖 : Set (Set α)
is nonempty and directed, 𝓝 f
admits the
family {g | ∀ x ∈ S, (f x, g x) ∈ V}
for S ∈ 𝔖
and V ∈ 𝓑
as a filter basis, for any basis
𝓑
of 𝓤 β
.
For f : α →ᵤ[𝔖] β
, where 𝔖 : Set (Set α)
is nonempty and directed, 𝓝 f
admits the
family {g | ∀ x ∈ S, (f x, g x) ∈ V}
for S ∈ 𝔖
and V ∈ 𝓤 β
as a filter basis.
If S ∈ 𝔖
, then the restriction to S
is a uniformly continuous map from α →ᵤ[𝔖] β
to
↥S →ᵤ β
.
A version of UniformOnFun.hasBasis_uniformity_of_basis
with weaker conclusion and weaker assumptions.
We make no assumptions about the set 𝔖
but conclude only that the uniformity is equal to some indexed infimum.
A version of UniformOnFun.hasBasis_nhds_of_basis
with weaker conclusion and weaker assumptions.
We make no assumptions about the set 𝔖
but conclude only that the neighbourhoods filter is equal to some indexed infimum.
The uniformity on α →ᵤ[𝔖] β
is the same as the uniformity on α →ᵤ β
,
provided that Set.univ ∈ 𝔖
.
Here we formulate it as a UniformEquiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Let u₁
, u₂
be two uniform structures on γ
and 𝔖₁ 𝔖₂ : Set (Set α)
. If u₁ ≤ u₂
and
𝔖₂ ⊆ 𝔖₁
then 𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂)
.
If x : α
is in some S ∈ 𝔖
, then evaluation at x
is uniformly continuous on
α →ᵤ[𝔖] β
.
If u
is a family of uniform structures on γ
, then
𝒱(α, γ, 𝔖, (⨅ i, u i)) = ⨅ i, 𝒱(α, γ, 𝔖, u i)
.
If u₁
and u₂
are two uniform structures on γ
, then
𝒱(α, γ, 𝔖, u₁ ⊓ u₂) = 𝒱(α, γ, 𝔖, u₁) ⊓ 𝒱(α, γ, 𝔖, u₂)
.
If u
is a uniform structure on β
and f : γ → β
, then
𝒱(α, γ, 𝔖, comap f u) = comap (fun g ↦ f ∘ g) 𝒱(α, γ, 𝔖, u₁)
.
Post-composition by a uniformly continuous function is uniformly continuous for the
uniform structures of 𝔖
-convergence.
More precisely, if f : γ → β
is uniformly continuous, then
(fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β)
is uniformly continuous.
Post-composition by a uniform inducing is a uniform inducing for the
uniform structures of 𝔖
-convergence.
More precisely, if f : γ → β
is a uniform inducing, then
(fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β)
is a uniform inducing.
Post-composition by a uniform embedding is a uniform embedding for the
uniform structures of 𝔖
-convergence.
More precisely, if f : γ → β
is a uniform embedding, then
(fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β)
is a uniform embedding.
Alias of UniformOnFun.postcomp_isUniformEmbedding
.
Post-composition by a uniform embedding is a uniform embedding for the
uniform structures of 𝔖
-convergence.
More precisely, if f : γ → β
is a uniform embedding, then
(fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β)
is a uniform embedding.
Turn a uniform isomorphism γ ≃ᵤ β
into a uniform isomorphism (α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β)
by post-composing.
Equations
- UniformOnFun.congrRight e = { toEquiv := Equiv.piCongrRight fun (_a : α) => e.toEquiv, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
Instances For
Let f : γ → α
, 𝔖 : Set (Set α)
, 𝔗 : Set (Set γ)
, and assume that ∀ T ∈ 𝔗, f '' T ∈ 𝔖
.
Then, the function (fun g ↦ g ∘ f) : (α →ᵤ[𝔖] β) → (γ →ᵤ[𝔗] β)
is uniformly continuous.
Note that one can easily see that assuming ∀ T ∈ 𝔗, ∃ S ∈ 𝔖, f '' T ⊆ S
would work too, but
we will get this for free when we prove that 𝒱(α, β, 𝔖, uβ) = 𝒱(α, β, 𝔖', uβ)
where 𝔖'
is the
noncovering bornology generated by 𝔖
.
Turn a bijection e : γ ≃ α
such that we have both ∀ T ∈ 𝔗, e '' T ∈ 𝔖
and
∀ S ∈ 𝔖, e ⁻¹' S ∈ 𝔗
into a uniform isomorphism (γ →ᵤ[𝔗] β) ≃ᵤ (α →ᵤ[𝔖] β)
by pre-composing.
Equations
- UniformOnFun.congrLeft e he he' = { toEquiv := e.arrowCongr (Equiv.refl β), uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
Instances For
If 𝔖
covers α
, then the topology of 𝔖
-convergence is T₂.
The restriction map from α →ᵤ[𝔖] β
to ⋃₀ 𝔖 → β
is uniformly continuous.
If 𝔖
covers α
, the natural map UniformOnFun.toFun
from α →ᵤ[𝔖] β
to α → β
is
uniformly continuous.
In other words, if 𝔖
covers α
, then the uniform structure of 𝔖
-convergence is finer than
that of pointwise convergence.
If f : α →ᵤ[𝔖] β
is continuous at x
and x
admits a neighbourhood V ∈ 𝔖
,
then evaluation of g : α →ᵤ[𝔖] β
at y : α
is continuous in (g, y)
at (f, x)
.
If each point of α
admits a neighbourhood V ∈ 𝔖
,
then the evaluation of f : α →ᵤ[𝔖] β
at x : α
is continuous in (f, x)
on the set of (f, x)
such that f
is continuous at x
.
Convergence in the topology of 𝔖
-convergence means uniform convergence on S
(in the sense
of TendstoUniformlyOn
) for all S ∈ 𝔖
.
Equations
- ⋯ = ⋯
The natural bijection between α → β × γ
and (α → β) × (α → γ)
, upgraded to a uniform
isomorphism between α →ᵤ[𝔖] β × γ
and (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The natural bijection between α → Π i, δ i
and Π i, α → δ i
, upgraded to a uniform
isomorphism between α →ᵤ[𝔖] (Π i, δ i)
and Π i, α →ᵤ[𝔖] δ i
.
Equations
- UniformOnFun.uniformEquivPiComm 𝔖 δ = (Equiv.piComm fun (a : α) => δ).toUniformEquivOfUniformInducing ⋯
Instances For
Suppose that the topology on α
is defined by its restrictions to the sets of 𝔖
.
Then the set of continuous functions is closed
in the topology of uniform convergence on the sets of 𝔖
.
Suppose that the topology on α
is defined by its restrictions to the sets of 𝔖
.
Then the set of continuous functions is closed
in the topology of uniform convergence on the sets of 𝔖
.
Equations
- ⋯ = ⋯