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 Equiv : Type (max u_4 u_5)

• 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 β

def «term_≃ᵤ_» : Lean.TrailingParserDescr

Uniform isomorphism between α and β

theorem UniformEquiv.toEquiv_injective {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] : Function.Injective UniformEquiv.toEquiv

instance UniformEquiv.instEquivLikeUniformEquiv {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] : EquivLike (α ≃ᵤ β) α β

@[simp]

theorem UniformEquiv.uniformEquiv_mk_coe {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (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} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) : β ≃ᵤ α

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.

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

See Note [custom simps projection]

@[simp]

theorem UniformEquiv.coe_toEquiv {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) : ↑h.toEquiv = ↑h

@[simp]

theorem UniformEquiv.coe_symm_toEquiv {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) : ↑h.symm = ↑(UniformEquiv.symm h)

theorem UniformEquiv.ext {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] {h : α ≃ᵤ β} {h' : α ≃ᵤ β} (H : ∀ (x : α), ↑h x = ↑h' x) : h = h'

@[simp]

theorem UniformEquiv.refl_apply (α : Type u_4) [UniformSpace α] : ↑(UniformEquiv.refl α) = id

def UniformEquiv.refl (α : Type u_4) [UniformSpace α] : α ≃ᵤ α

Identity map as a uniform isomorphism.

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 : α) : ↑(UniformEquiv.trans h₁ h₂) a = ↑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) : ↑(UniformEquiv.symm { toEquiv := a, uniformContinuous_toFun := b, uniformContinuous_invFun := c }) = ↑a.symm

@[simp]

theorem UniformEquiv.refl_symm {α : Type u} [UniformSpace α] : UniformEquiv.symm (UniformEquiv.refl α) = UniformEquiv.refl α

theorem UniformEquiv.uniformContinuous {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) : UniformContinuous ↑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 : α ≃ᵤ β) : UniformContinuous ↑(UniformEquiv.symm h)

theorem UniformEquiv.continuous_symm {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) : Continuous ↑(UniformEquiv.symm h)

def UniformEquiv.toHomeomorph {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (e : α ≃ᵤ β) : α ≃ₜ β

A uniform isomorphism as a homeomorphism.

theorem UniformEquiv.toHomeomorph_apply {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (e : α ≃ᵤ β) : ↑(UniformEquiv.toHomeomorph e) = ↑e

theorem UniformEquiv.toHomeomorph_symm_apply {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (e : α ≃ᵤ β) : ↑(Homeomorph.symm (UniformEquiv.toHomeomorph e)) = ↑(UniformEquiv.symm e)

@[simp]

theorem UniformEquiv.apply_symm_apply {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) (x : β) : ↑h (↑(UniformEquiv.symm h) x) = x

@[simp]

theorem UniformEquiv.symm_apply_apply {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) (x : α) : ↑(UniformEquiv.symm h) (↑h x) = x

theorem UniformEquiv.bijective {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) : Function.Bijective ↑h

theorem UniformEquiv.injective {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) : Function.Injective ↑h

theorem UniformEquiv.surjective {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) : Function.Surjective ↑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 : α ≃ᵤ β) : ↑(UniformEquiv.symm h) ∘ ↑h = id

@[simp]

theorem UniformEquiv.self_comp_symm {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) : ↑h ∘ ↑(UniformEquiv.symm h) = id

theorem UniformEquiv.range_coe {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) : Set.range ↑h = Set.univ

theorem UniformEquiv.image_symm {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) : Set.image ↑(UniformEquiv.symm h) = Set.preimage ↑h

theorem UniformEquiv.preimage_symm {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) : Set.preimage ↑(UniformEquiv.symm h) = Set.image ↑h

theorem UniformEquiv.image_preimage {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) (s : Set β) : ↑h '' (↑h ⁻¹' s) = s

theorem UniformEquiv.preimage_image {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) (s : Set α) : ↑h ⁻¹' (↑h '' s) = s

theorem UniformEquiv.uniformInducing {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) : UniformInducing ↑h

theorem UniformEquiv.comap_eq {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) : UniformSpace.comap (↑h) inst✝ = inst✝¹

theorem UniformEquiv.uniformEmbedding {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) : UniformEmbedding ↑h

noncomputable def UniformEquiv.ofUniformEmbedding {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (f : α → β) (hf : UniformEmbedding f) : α ≃ᵤ ↑(Set.range f)

Uniform equiv given a uniform embedding.

def UniformEquiv.setCongr {α : Type u} [UniformSpace α] {s : Set α} {t : Set α} (h : s = t) : ↑s ≃ᵤ ↑t

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

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₂ : γ ≃ᵤ δ) : UniformEquiv.symm (UniformEquiv.prodCongr h₁ h₂) = UniformEquiv.prodCongr (UniformEquiv.symm h₁) (UniformEquiv.symm h₂)

@[simp]

theorem UniformEquiv.coe_prodCongr {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} [UniformSpace α] [UniformSpace β] [UniformSpace γ] [UniformSpace δ] (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) : ↑(UniformEquiv.prodCongr h₁ h₂) = Prod.map ↑h₁ ↑h₂

def UniformEquiv.prodComm (α : Type u) (β : Type u_1) [UniformSpace α] [UniformSpace β] : α × β ≃ᵤ β × α

α × β is uniformly isomorphic to β × α.

@[simp]

theorem UniformEquiv.prodComm_symm (α : Type u) (β : Type u_1) [UniformSpace α] [UniformSpace β] : UniformEquiv.symm (UniformEquiv.prodComm α β) = UniformEquiv.prodComm β α

@[simp]

theorem UniformEquiv.coe_prodComm (α : Type u) (β : Type u_1) [UniformSpace α] [UniformSpace β] : ↑(UniformEquiv.prodComm α β) = Prod.swap

def UniformEquiv.prodAssoc (α : Type u) (β : Type u_1) (γ : Type u_2) [UniformSpace α] [UniformSpace β] [UniformSpace γ] : (α × β) × γ ≃ᵤ α × β × γ

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

@[simp]

theorem UniformEquiv.prodPunit_apply (α : Type u) [UniformSpace α] : ↑(UniformEquiv.prodPunit α) = fun p => p.fst

def UniformEquiv.prodPunit (α : Type u) [UniformSpace α] : α × PUnit.{u_4 + 1} ≃ᵤ α

α × {*} is uniformly isomorphic to α.

def UniformEquiv.punitProd (α : Type u) [UniformSpace α] : PUnit.{u_4 + 1} × α ≃ᵤ α

{*} × α is uniformly isomorphic to α.

@[simp]

theorem UniformEquiv.coe_punitProd (α : Type u) [UniformSpace α] : ↑(UniformEquiv.punitProd α) = 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 : ι'), ↑(UniformEquiv.piCongrLeft e) 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 : ι ≃ ι') : (UniformEquiv.piCongrLeft e).toEquiv = Equiv.piCongrLeft β e

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 ι ≃ ι'.

@[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 : ι) → (fun i => β₁ i) a) (a : ι) : ↑(UniformEquiv.piCongrRight F) H 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) : (UniformEquiv.piCongrRight F).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.

@[simp]

theorem UniformEquiv.piCongrRight_symm {ι : Type u_4} {β₁ : ι → Type u_5} {β₂ : ι → Type u_6} [(i : ι) → UniformSpace (β₁ i)] [(i : ι) → UniformSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ᵤ β₂ i) : UniformEquiv.symm (UniformEquiv.piCongrRight F) = UniformEquiv.piCongrRight fun i => UniformEquiv.symm (F i)

@[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₁)) : (UniformEquiv.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₂ : ι₂), ↑(UniformEquiv.piCongr e F) a i₂ = (_ : ↑e (↑e.symm i₂) = 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₁ : ι₁.

def UniformEquiv.ulift (α : Type u) [UniformSpace α] : ULift.{v, u} α ≃ᵤ α

Uniform equivalence between ULift α and α.

@[simp]

theorem UniformEquiv.funUnique_apply (ι : Type u_4) (α : Type u_5) [Unique ι] [UniformSpace α] : ↑(UniformEquiv.funUnique ι α) = fun f => f default

@[simp]

theorem UniformEquiv.funUnique_symm_apply (ι : Type u_4) (α : Type u_5) [Unique ι] [UniformSpace α] : ↑(UniformEquiv.symm (UniformEquiv.funUnique ι α)) = fun x b => x

def UniformEquiv.funUnique (ι : Type u_4) (α : Type u_5) [Unique ι] [UniformSpace α] : (ι → α) ≃ᵤ α

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

@[simp]

theorem UniformEquiv.piFinTwo_symm_apply (α : Fin 2 → Type u) [(i : Fin 2) → UniformSpace (α i)] : ↑(UniformEquiv.symm (UniformEquiv.piFinTwo α)) = fun p => Fin.cons p.fst (Fin.cons p.snd finZeroElim)

@[simp]

theorem UniformEquiv.piFinTwo_apply (α : Fin 2 → Type u) [(i : Fin 2) → UniformSpace (α i)] : ↑(UniformEquiv.piFinTwo α) = fun f => (f 0, f 1)

def UniformEquiv.piFinTwo (α : Fin 2 → Type u) [(i : Fin 2) → UniformSpace (α i)] : ((i : Fin 2) → α i) ≃ᵤ α 0 × α 1

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

@[simp]

theorem UniformEquiv.finTwoArrow_symm_apply (α : Type u_4) [UniformSpace α] : ↑(UniformEquiv.symm (UniformEquiv.finTwoArrow α)) = fun x => ![x.fst, x.snd]

@[simp]

theorem UniformEquiv.finTwoArrow_apply (α : Type u_4) [UniformSpace α] : ↑(UniformEquiv.finTwoArrow α) = fun f => (f 0, f 1)

def UniformEquiv.finTwoArrow (α : Type u_4) [UniformSpace α] : (Fin 2 → α) ≃ᵤ α × α

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

def UniformEquiv.image {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (e : α ≃ᵤ β) (s : Set α) : ↑s ≃ᵤ ↑(↑e '' s)

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

def Equiv.toUniformEquivOfUniformInducing {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (f : α ≃ β) (hf : UniformInducing ↑f) : α ≃ᵤ β

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