Uniform isomorphisms #
This file defines uniform isomorphisms between two uniform spaces. They are bijections with both
directions uniformly continuous. We denote uniform isomorphisms with the notation ≃ᵤ
.
Main definitions #
UniformEquiv α β
: The type of uniform isomorphisms fromα
toβ
. This type can be denoted using the following notation:α ≃ᵤ β
.
- toFun : α → β
- invFun : β → α
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
- uniformContinuous_toFun : UniformContinuous s.toFun
Uniform continuity of the function
- uniformContinuous_invFun : UniformContinuous s.invFun
Uniform continuity of the inverse
Uniform isomorphism between α
and β
Instances For
Inverse of a uniform isomorphism.
Instances For
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Instances For
See Note [custom simps projection]
Instances For
Identity map as a uniform isomorphism.
Instances For
Composition of two uniform isomorphisms.
Instances For
A uniform isomorphism as a homeomorphism.
Instances For
Change the uniform equiv f
to make the inverse function definitionally equal to g
.
Instances For
Uniform equiv given a uniform embedding.
Instances For
If two sets are equal, then they are uniformly equivalent.
Instances For
Product of two uniform isomorphisms.
Instances For
α × β
is uniformly isomorphic to β × α
.
Instances For
(α × β) × γ
is uniformly isomorphic to α × (β × γ)
.
Instances For
α × {*}
is uniformly isomorphic to α
.
Instances For
{*} × α
is uniformly isomorphic to α
.
Instances For
Equiv.piCongrLeft
as a uniform isomorphism: this is the natural isomorphism
Π i, β (e i) ≃ᵤ Π j, β j
obtained from a bijection ι ≃ ι'
.
Instances For
Equiv.piCongrRight
as a uniform isomorphism: this is the natural isomorphism
Π i, β₁ i ≃ᵤ Π j, β₂ i
obtained from uniform isomorphisms β₁ i ≃ᵤ β₂ i
for each i
.
Instances For
Equiv.piCongr
as a uniform isomorphism: this is the natural isomorphism
Π i₁, β₁ i ≃ᵤ Π i₂, β₂ i₂
obtained from a bijection ι₁ ≃ ι₂
and isomorphisms
β₁ i₁ ≃ᵤ β₂ (e i₁)
for each i₁ : ι₁
.
Instances For
Uniform equivalence between ULift α
and α
.
Instances For
If ι
has a unique element, then ι → α
is uniformly isomorphic to α
.
Instances For
Uniform isomorphism between dependent functions Π i : Fin 2, α i
and α 0 × α 1
.
Instances For
Uniform isomorphism between α² = Fin 2 → α
and α × α
.
Instances For
A subset of a uniform space is uniformly isomorphic to its image under a uniform isomorphism.
Instances For
A uniform inducing equiv between uniform spaces is a uniform isomorphism.