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: α ≃ᵤ β.
structure UniformEquiv (α : Type u_4) (β : Type u_5) [] [] extends :
Type (max u_4 u_5)

Uniform isomorphism between α and β

Instances For
theorem UniformEquiv.uniformContinuous_toFun {α : Type u_4} {β : Type u_5} [] [] (self : α ≃ᵤ β) :

Uniform continuity of the function

theorem UniformEquiv.uniformContinuous_invFun {α : Type u_4} {β : Type u_5} [] [] (self : α ≃ᵤ β) :
UniformContinuous self.invFun

Uniform continuity of the inverse

Uniform isomorphism between α and β

Equations
Instances For
theorem UniformEquiv.toEquiv_injective {α : Type u} {β : Type u_1} [] [] :
Function.Injective UniformEquiv.toEquiv
instance UniformEquiv.instEquivLike {α : Type u} {β : Type u_1} [] [] :
EquivLike (α ≃ᵤ β) α β
Equations
• UniformEquiv.instEquivLike = { coe := fun (h : α ≃ᵤ β) => h.toEquiv, inv := fun (h : α ≃ᵤ β) => h.symm, left_inv := , right_inv := , coe_injective' := }
@[simp]
theorem UniformEquiv.uniformEquiv_mk_coe {α : Type u} {β : Type u_1} [] [] (a : α β) (b : UniformContinuous a.toFun) (c : UniformContinuous a.invFun) :
{ toEquiv := a, uniformContinuous_toFun := b, uniformContinuous_invFun := c } = a
def UniformEquiv.symm {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
β ≃ᵤ α

Inverse of a uniform isomorphism.

Equations
• h.symm = { toEquiv := h.symm, uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For
def UniformEquiv.Simps.apply {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
αβ

See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

Equations
Instances For
def UniformEquiv.Simps.symm_apply {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
βα

See Note [custom simps projection]

Equations
• = h.symm
Instances For
@[simp]
theorem UniformEquiv.coe_toEquiv {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
h.toEquiv = h
@[simp]
theorem UniformEquiv.coe_symm_toEquiv {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
h.symm = h.symm
theorem UniformEquiv.ext_iff {α : Type u} {β : Type u_1} [] [] {h : α ≃ᵤ β} {h' : α ≃ᵤ β} :
h = h' ∀ (x : α), h x = h' x
theorem UniformEquiv.ext {α : Type u} {β : Type u_1} [] [] {h : α ≃ᵤ β} {h' : α ≃ᵤ β} (H : ∀ (x : α), h x = h' x) :
h = h'
@[simp]
theorem UniformEquiv.refl_apply (α : Type u_4) [] :
= id
def UniformEquiv.refl (α : Type u_4) [] :
α ≃ᵤ α

Identity map as a uniform isomorphism.

Equations
• = { toEquiv := , uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For
def UniformEquiv.trans {α : Type u} {β : Type u_1} {γ : Type u_2} [] [] [] (h₁ : α ≃ᵤ β) (h₂ : β ≃ᵤ γ) :
α ≃ᵤ γ

Composition of two uniform isomorphisms.

Equations
• h₁.trans h₂ = { toEquiv := h₁.trans h₂.toEquiv, uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For
@[simp]
theorem UniformEquiv.trans_apply {α : Type u} {β : Type u_1} {γ : Type u_2} [] [] [] (h₁ : α ≃ᵤ β) (h₂ : β ≃ᵤ γ) (a : α) :
(h₁.trans h₂) a = h₂ (h₁ a)
@[simp]
theorem UniformEquiv.uniformEquiv_mk_coe_symm {α : Type u} {β : Type u_1} [] [] (a : α β) (b : UniformContinuous a.toFun) (c : UniformContinuous a.invFun) :
{ toEquiv := a, uniformContinuous_toFun := b, uniformContinuous_invFun := c }.symm = a.symm
@[simp]
theorem UniformEquiv.refl_symm {α : Type u} [] :
.symm =
theorem UniformEquiv.uniformContinuous {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
theorem UniformEquiv.continuous {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
theorem UniformEquiv.uniformContinuous_symm {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
theorem UniformEquiv.continuous_symm {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
Continuous h.symm
def UniformEquiv.toHomeomorph {α : Type u} {β : Type u_1} [] [] (e : α ≃ᵤ β) :
α ≃ₜ β

A uniform isomorphism as a homeomorphism.

Equations
• e.toHomeomorph = let __src := e.toEquiv; { toEquiv := __src, continuous_toFun := , continuous_invFun := }
Instances For
theorem UniformEquiv.toHomeomorph_apply {α : Type u} {β : Type u_1} [] [] (e : α ≃ᵤ β) :
e.toHomeomorph = e
theorem UniformEquiv.toHomeomorph_symm_apply {α : Type u} {β : Type u_1} [] [] (e : α ≃ᵤ β) :
e.toHomeomorph.symm = e.symm
@[simp]
theorem UniformEquiv.apply_symm_apply {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) (x : β) :
h (h.symm x) = x
@[simp]
theorem UniformEquiv.symm_apply_apply {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) (x : α) :
h.symm (h x) = x
theorem UniformEquiv.bijective {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
theorem UniformEquiv.injective {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
theorem UniformEquiv.surjective {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
def UniformEquiv.changeInv {α : Type u} {β : Type u_1} [] [] (f : α ≃ᵤ β) (g : βα) (hg : ) :
α ≃ᵤ β

Change the uniform equiv f to make the inverse function definitionally equal to g.

Equations
• f.changeInv g hg = let_fun this := ; { toFun := f, invFun := g, left_inv := , right_inv := , uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For
@[simp]
theorem UniformEquiv.symm_comp_self {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
h.symm h = id
@[simp]
theorem UniformEquiv.self_comp_symm {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
h h.symm = id
theorem UniformEquiv.range_coe {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
= Set.univ
theorem UniformEquiv.image_symm {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
Set.image h.symm =
theorem UniformEquiv.preimage_symm {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
Set.preimage h.symm =
theorem UniformEquiv.image_preimage {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) (s : Set β) :
h '' (h ⁻¹' s) = s
theorem UniformEquiv.preimage_image {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) (s : Set α) :
h ⁻¹' (h '' s) = s
theorem UniformEquiv.uniformInducing {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
theorem UniformEquiv.comap_eq {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
UniformSpace.comap (⇑h) inst✝ = inst✝¹
theorem UniformEquiv.uniformEmbedding {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
theorem UniformEquiv.completeSpace_iff {α : Type u} {β : Type u_1} [] [] (h : α ≃ᵤ β) :
noncomputable def UniformEquiv.ofUniformEmbedding {α : Type u} {β : Type u_1} [] [] (f : αβ) (hf : ) :
α ≃ᵤ (Set.range f)

Uniform equiv given a uniform embedding.

Equations
• = { toEquiv := , uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For
def UniformEquiv.setCongr {α : Type u} [] {s : Set α} {t : Set α} (h : s = t) :
s ≃ᵤ t

If two sets are equal, then they are uniformly equivalent.

Equations
• = { toEquiv := , uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For
def UniformEquiv.prodCongr {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} [] [] [] [] (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) :
α × γ ≃ᵤ β × δ

Product of two uniform isomorphisms.

Equations
• h₁.prodCongr h₂ = { toEquiv := h₁.prodCongr h₂.toEquiv, uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For
@[simp]
theorem UniformEquiv.prodCongr_symm {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} [] [] [] [] (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) :
(h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm
@[simp]
theorem UniformEquiv.coe_prodCongr {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} [] [] [] [] (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) :
(h₁.prodCongr h₂) = Prod.map h₁ h₂
def UniformEquiv.prodComm (α : Type u) (β : Type u_1) [] [] :
α × β ≃ᵤ β × α

α × β is uniformly isomorphic to β × α.

Equations
• = { toEquiv := , uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For
@[simp]
theorem UniformEquiv.prodComm_symm (α : Type u) (β : Type u_1) [] [] :
.symm =
@[simp]
theorem UniformEquiv.coe_prodComm (α : Type u) (β : Type u_1) [] [] :
= Prod.swap
def UniformEquiv.prodAssoc (α : Type u) (β : Type u_1) (γ : Type u_2) [] [] [] :
(α × β) × γ ≃ᵤ α × β × γ

(α × β) × γ is uniformly isomorphic to α × (β × γ).

Equations
• = { toEquiv := , uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For
@[simp]
theorem UniformEquiv.prodPunit_apply (α : Type u) [] :
= fun (p : ) => p.1
def UniformEquiv.prodPunit (α : Type u) [] :

α × {*} is uniformly isomorphic to α.

Equations
• = { toEquiv := , uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For
def UniformEquiv.punitProd (α : Type u) [] :
≃ᵤ α

{*} × α is uniformly isomorphic to α.

Equations
• = .trans
Instances For
@[simp]
theorem UniformEquiv.coe_punitProd (α : Type u) [] :
= Prod.snd
@[simp]
theorem UniformEquiv.piCongrLeft_apply {ι : Type u_4} {ι' : Type u_5} {β : ι'Type u_6} [(j : ι') → UniformSpace (β j)] (e : ι ι') :
∀ (a : (b : ι) → β (e.symm.symm b)) (a_1 : ι'), a a_1 = (Equiv.piCongrLeft' β e.symm).symm a a_1
@[simp]
theorem UniformEquiv.piCongrLeft_toEquiv {ι : Type u_4} {ι' : Type u_5} {β : ι'Type u_6} [(j : ι') → UniformSpace (β j)] (e : ι ι') :
.toEquiv =
def UniformEquiv.piCongrLeft {ι : Type u_4} {ι' : Type u_5} {β : ι'Type u_6} [(j : ι') → UniformSpace (β j)] (e : ι ι') :
((i : ι) → β (e i)) ≃ᵤ ((j : ι') → β j)

Equiv.piCongrLeft as a uniform isomorphism: this is the natural isomorphism Π i, β (e i) ≃ᵤ Π j, β j obtained from a bijection ι ≃ ι'.

Equations
• = { toEquiv := , uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For
@[simp]
theorem UniformEquiv.piCongrRight_apply {ι : Type u_4} {β₁ : ιType u_5} {β₂ : ιType u_6} [(i : ι) → UniformSpace (β₁ i)] [(i : ι) → UniformSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ᵤ β₂ i) (H : (a : ι) → β₁ a) (a : ι) :
= (F a) (H a)
@[simp]
theorem UniformEquiv.piCongrRight_toEquiv {ι : Type u_4} {β₁ : ιType u_5} {β₂ : ιType u_6} [(i : ι) → UniformSpace (β₁ i)] [(i : ι) → UniformSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ᵤ β₂ i) :
.toEquiv = Equiv.piCongrRight fun (i : ι) => (F i).toEquiv
def UniformEquiv.piCongrRight {ι : Type u_4} {β₁ : ιType u_5} {β₂ : ιType u_6} [(i : ι) → UniformSpace (β₁ i)] [(i : ι) → UniformSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ᵤ β₂ i) :
((i : ι) → β₁ i) ≃ᵤ ((i : ι) → β₂ i)

Equiv.piCongrRight as a uniform isomorphism: this is the natural isomorphism Π i, β₁ i ≃ᵤ Π j, β₂ i obtained from uniform isomorphisms β₁ i ≃ᵤ β₂ i for each i.

Equations
• = { toEquiv := Equiv.piCongrRight fun (i : ι) => (F i).toEquiv, uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For
@[simp]
theorem UniformEquiv.piCongrRight_symm {ι : Type u_4} {β₁ : ιType u_5} {β₂ : ιType u_6} [(i : ι) → UniformSpace (β₁ i)] [(i : ι) → UniformSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ᵤ β₂ i) :
.symm = UniformEquiv.piCongrRight fun (i : ι) => (F i).symm
@[simp]
theorem UniformEquiv.piCongr_toEquiv {ι₁ : Type u_4} {ι₂ : Type u_5} {β₁ : ι₁Type u_6} {β₂ : ι₂Type u_7} [(i₁ : ι₁) → UniformSpace (β₁ i₁)] [(i₂ : ι₂) → UniformSpace (β₂ i₂)] (e : ι₁ ι₂) (F : (i₁ : ι₁) → β₁ i₁ ≃ᵤ β₂ (e i₁)) :
.toEquiv = (Equiv.piCongrRight fun (i : ι₁) => (F i).toEquiv).trans (Equiv.piCongrLeft β₂ e)
@[simp]
theorem UniformEquiv.piCongr_apply {ι₁ : Type u_4} {ι₂ : Type u_5} {β₁ : ι₁Type u_6} {β₂ : ι₂Type u_7} [(i₁ : ι₁) → UniformSpace (β₁ i₁)] [(i₂ : ι₂) → UniformSpace (β₂ i₂)] (e : ι₁ ι₂) (F : (i₁ : ι₁) → β₁ i₁ ≃ᵤ β₂ (e i₁)) :
∀ (a : (i : ι₁) → β₁ i) (i₂ : ι₂), a i₂ = (Equiv.piCongrRight fun (i : ι₁) => (F i).toEquiv) a (e.symm i₂)
def UniformEquiv.piCongr {ι₁ : Type u_4} {ι₂ : Type u_5} {β₁ : ι₁Type u_6} {β₂ : ι₂Type u_7} [(i₁ : ι₁) → UniformSpace (β₁ i₁)] [(i₂ : ι₂) → UniformSpace (β₂ i₂)] (e : ι₁ ι₂) (F : (i₁ : ι₁) → β₁ i₁ ≃ᵤ β₂ (e i₁)) :
((i₁ : ι₁) → β₁ i₁) ≃ᵤ ((i₂ : ι₂) → β₂ i₂)

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₁ : ι₁.

Equations
• = .trans
Instances For
def UniformEquiv.ulift (α : Type u) [] :
≃ᵤ α

Uniform equivalence between ULift α and α.

Equations
• = let __src := Equiv.ulift; { toEquiv := __src, uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For
@[simp]
theorem UniformEquiv.funUnique_apply (ι : Type u_4) (α : Type u_5) [] [] :
= fun (f : ια) => f default
@[simp]
theorem UniformEquiv.funUnique_symm_apply (ι : Type u_4) (α : Type u_5) [] [] :
.symm = uniqueElim
def UniformEquiv.funUnique (ι : Type u_4) (α : Type u_5) [] [] :
(ια) ≃ᵤ α

If ι has a unique element, then ι → α is uniformly isomorphic to α.

Equations
• = { toEquiv := , uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For
@[simp]
theorem UniformEquiv.piFinTwo_apply (α : Fin 2Type u) [(i : Fin 2) → UniformSpace (α i)] :
= fun (f : (i : Fin 2) → α i) => (f 0, f 1)
@[simp]
theorem UniformEquiv.piFinTwo_symm_apply (α : Fin 2Type u) [(i : Fin 2) → UniformSpace (α i)] :
.symm = fun (p : α 0 × α 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
def UniformEquiv.piFinTwo (α : Fin 2Type u) [(i : Fin 2) → UniformSpace (α i)] :
((i : Fin 2) → α i) ≃ᵤ α 0 × α 1

Uniform isomorphism between dependent functions Π i : Fin 2, α i and α 0 × α 1.

Equations
• = { toEquiv := , uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For
@[simp]
theorem UniformEquiv.finTwoArrow_apply (α : Type u_4) [] :
= fun (f : Fin 2α) => (f 0, f 1)
@[simp]
theorem UniformEquiv.finTwoArrow_symm_apply (α : Type u_4) [] :
.symm = fun (x : α × α) => ![x.1, x.2]
def UniformEquiv.finTwoArrow (α : Type u_4) [] :
(Fin 2α) ≃ᵤ α × α

Uniform isomorphism between α² = Fin 2 → α and α × α.

Equations
• = let __src := UniformEquiv.piFinTwo fun (x : Fin 2) => α; { toEquiv := , uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For
def UniformEquiv.image {α : Type u} {β : Type u_1} [] [] (e : α ≃ᵤ β) (s : Set α) :
s ≃ᵤ (e '' s)

A subset of a uniform space is uniformly isomorphic to its image under a uniform isomorphism.

Equations
• e.image s = { toEquiv := e.image s, uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For
def Equiv.toUniformEquivOfUniformInducing {α : Type u} {β : Type u_1} [] [] (f : α β) (hf : ) :
α ≃ᵤ β

A uniform inducing equiv between uniform spaces is a uniform isomorphism.

Equations
• f.toUniformEquivOfUniformInducing hf = { toEquiv := f, uniformContinuous_toFun := , uniformContinuous_invFun := }
Instances For