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)
[UniformSpace α]
[UniformSpace β]
extends α ≃ β :
Type (max u_4 u_5)
Uniform isomorphism between α and β
- toFun : α → β
- invFun : β → α
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
- uniformContinuous_toFun : UniformContinuous self.toFun
Uniform continuity of the function
- uniformContinuous_invFun : UniformContinuous self.invFun
Uniform continuity of the inverse
Uniform isomorphism between α and β
Equations
- «term_≃ᵤ_» = Lean.ParserDescr.trailingNode `«term_≃ᵤ_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ᵤ ") (Lean.ParserDescr.cat `term 26))
theorem
UniformEquiv.toEquiv_injective
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
:
@[simp]
theorem
UniformEquiv.uniformEquiv_mk_coe
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(a : α ≃ β)
(b : UniformContinuous a.toFun)
(c : UniformContinuous a.invFun)
:
Inverse of a uniform isomorphism.
def
UniformEquiv.Simps.apply
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(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
def
UniformEquiv.Simps.symm_apply
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
β → α
See Note [custom simps projection]
Equations
@[simp]
theorem
UniformEquiv.coe_toEquiv
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
@[simp]
theorem
UniformEquiv.coe_symm_toEquiv
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
theorem
UniformEquiv.ext
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
{h h' : α ≃ᵤ β}
(H : ∀ (x : α), h x = h' x)
:
theorem
UniformEquiv.ext_iff
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
{h h' : α ≃ᵤ β}
:
Identity map as a uniform isomorphism.
Equations
- UniformEquiv.refl α = { toEquiv := Equiv.refl α, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
@[simp]
def
UniformEquiv.trans
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
(h₁ : α ≃ᵤ β)
(h₂ : β ≃ᵤ γ)
:
Composition of two uniform isomorphisms.
@[simp]
theorem
UniformEquiv.trans_apply
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
(h₁ : α ≃ᵤ β)
(h₂ : β ≃ᵤ γ)
(a : α)
:
@[simp]
theorem
UniformEquiv.uniformEquiv_mk_coe_symm
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(a : α ≃ β)
(b : UniformContinuous a.toFun)
(c : UniformContinuous a.invFun)
:
@[simp]
theorem
UniformEquiv.uniformContinuous
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
theorem
UniformEquiv.continuous
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
Continuous ⇑h
theorem
UniformEquiv.uniformContinuous_symm
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
theorem
UniformEquiv.continuous_symm
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
Continuous ⇑h.symm
def
UniformEquiv.toHomeomorph
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(e : α ≃ᵤ β)
:
A uniform isomorphism as a homeomorphism.
Equations
- e.toHomeomorph = { toEquiv := e.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
theorem
UniformEquiv.toHomeomorph_apply
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(e : α ≃ᵤ β)
:
theorem
UniformEquiv.toHomeomorph_symm_apply
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(e : α ≃ᵤ β)
:
@[simp]
theorem
UniformEquiv.apply_symm_apply
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
(x : β)
:
@[simp]
theorem
UniformEquiv.symm_apply_apply
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
(x : α)
:
theorem
UniformEquiv.bijective
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
theorem
UniformEquiv.injective
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
theorem
UniformEquiv.surjective
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
def
UniformEquiv.changeInv
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(f : α ≃ᵤ β)
(g : β → α)
(hg : Function.RightInverse g ⇑f)
:
Change the uniform equiv f to make the inverse function definitionally equal to g.
@[simp]
theorem
UniformEquiv.symm_comp_self
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
@[simp]
theorem
UniformEquiv.self_comp_symm
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
theorem
UniformEquiv.range_coe
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
theorem
UniformEquiv.image_symm
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
theorem
UniformEquiv.preimage_symm
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
@[simp]
theorem
UniformEquiv.image_preimage
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
(s : Set β)
:
@[simp]
theorem
UniformEquiv.preimage_image
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
(s : Set α)
:
theorem
UniformEquiv.isUniformInducing
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
theorem
UniformEquiv.comap_eq
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
theorem
UniformEquiv.isUniformEmbedding
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
theorem
UniformEquiv.completeSpace_iff
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(h : α ≃ᵤ β)
:
noncomputable def
UniformEquiv.ofIsUniformEmbedding
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(f : α → β)
(hf : IsUniformEmbedding f)
:
Uniform equiv given a uniform embedding.
Equations
- UniformEquiv.ofIsUniformEmbedding f hf = { toEquiv := Equiv.ofInjective f ⋯, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
If two sets are equal, then they are uniformly equivalent.
Equations
- UniformEquiv.setCongr h = { toEquiv := Equiv.setCongr h, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
def
UniformEquiv.prodCongr
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
{δ : Type u_3}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
[UniformSpace δ]
(h₁ : α ≃ᵤ β)
(h₂ : γ ≃ᵤ δ)
:
Product of two uniform isomorphisms.
@[simp]
theorem
UniformEquiv.prodCongr_symm
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
{δ : Type u_3}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
[UniformSpace δ]
(h₁ : α ≃ᵤ β)
(h₂ : γ ≃ᵤ δ)
:
@[simp]
theorem
UniformEquiv.coe_prodCongr
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
{δ : Type u_3}
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
[UniformSpace δ]
(h₁ : α ≃ᵤ β)
(h₂ : γ ≃ᵤ δ)
:
α × β is uniformly isomorphic to β × α.
Equations
- UniformEquiv.prodComm α β = { toEquiv := Equiv.prodComm α β, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
@[simp]
@[simp]
def
UniformEquiv.prodAssoc
(α : Type u)
(β : Type u_1)
(γ : Type u_2)
[UniformSpace α]
[UniformSpace β]
[UniformSpace γ]
:
(α × β) × γ is uniformly isomorphic to α × (β × γ).
Equations
- UniformEquiv.prodAssoc α β γ = { toEquiv := Equiv.prodAssoc α β γ, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
α × {*} is uniformly isomorphic to α.
Equations
- UniformEquiv.prodPunit α = { toEquiv := Equiv.prodPUnit α, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
@[simp]
{*} × α is uniformly isomorphic to α.
Equations
@[simp]
def
UniformEquiv.piCongrLeft
{ι : Type u_4}
{ι' : Type u_5}
{β : ι' → Type u_6}
[(j : ι') → UniformSpace (β j)]
(e : ι ≃ ι')
:
Equiv.piCongrLeft as a uniform isomorphism: this is the natural isomorphism
Π i, β (e i) ≃ᵤ Π j, β j obtained from a bijection ι ≃ ι'.
Equations
- UniformEquiv.piCongrLeft e = { toEquiv := Equiv.piCongrLeft β e, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
@[simp]
theorem
UniformEquiv.piCongrLeft_toEquiv
{ι : Type u_4}
{ι' : Type u_5}
{β : ι' → Type u_6}
[(j : ι') → UniformSpace (β j)]
(e : ι ≃ ι')
:
@[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 : ι')
:
def
UniformEquiv.piCongrRight
{ι : Type u_4}
{β₁ : ι → Type u_5}
{β₂ : ι → Type u_6}
[(i : ι) → UniformSpace (β₁ i)]
[(i : ι) → UniformSpace (β₂ i)]
(F : (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
- UniformEquiv.piCongrRight F = { toEquiv := Equiv.piCongrRight fun (i : ι) => (F i).toEquiv, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
@[simp]
theorem
UniformEquiv.piCongrRight_toEquiv
{ι : Type u_4}
{β₁ : ι → Type u_5}
{β₂ : ι → Type u_6}
[(i : ι) → UniformSpace (β₁ i)]
[(i : ι) → UniformSpace (β₂ i)]
(F : (i : ι) → β₁ i ≃ᵤ β₂ i)
:
@[simp]
theorem
UniformEquiv.piCongrRight_apply
{ι : Type u_4}
{β₁ : ι → Type u_5}
{β₂ : ι → Type u_6}
[(i : ι) → UniformSpace (β₁ i)]
[(i : ι) → UniformSpace (β₂ i)]
(F : (i : ι) → β₁ i ≃ᵤ β₂ i)
(a✝ : (i : ι) → β₁ i)
(i : ι)
:
@[simp]
theorem
UniformEquiv.piCongrRight_symm
{ι : Type u_4}
{β₁ : ι → Type u_5}
{β₂ : ι → Type u_6}
[(i : ι) → UniformSpace (β₁ i)]
[(i : ι) → UniformSpace (β₂ i)]
(F : (i : ι) → β₁ i ≃ᵤ β₂ 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₁))
:
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
@[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₁))
:
(piCongr e F).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₂ : ι₂)
:
Uniform equivalence between ULift α and α.
Equations
- UniformEquiv.ulift α = { toEquiv := Equiv.ulift, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
If ι has a unique element, then ι → α is uniformly isomorphic to α.
Equations
- UniformEquiv.funUnique ι α = { toEquiv := Equiv.funUnique ι α, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
@[simp]
@[simp]
theorem
UniformEquiv.funUnique_symm_apply
(ι : Type u_4)
(α : Type u_5)
[Unique ι]
[UniformSpace α]
:
Uniform isomorphism between dependent functions Π i : Fin 2, α i and α 0 × α 1.
Equations
- UniformEquiv.piFinTwo α = { toEquiv := piFinTwoEquiv α, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
@[simp]
Uniform isomorphism between α² = Fin 2 → α and α × α.
Equations
- UniformEquiv.finTwoArrow α = { toEquiv := finTwoArrowEquiv α, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }
@[simp]
@[simp]
def
UniformEquiv.image
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(e : α ≃ᵤ β)
(s : Set α)
:
A subset of a uniform space is uniformly isomorphic to its image under a uniform isomorphism.
def
Equiv.toUniformEquivOfIsUniformInducing
{α : Type u}
{β : Type u_1}
[UniformSpace α]
[UniformSpace β]
(f : α ≃ β)
(hf : IsUniformInducing ⇑f)
:
A uniform inducing equiv between uniform spaces is a uniform isomorphism.
Equations
- f.toUniformEquivOfIsUniformInducing hf = { toEquiv := f, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }