# 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: `α ≃ᵤ β`.

source
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

Instances For

source
def «term_≃ᵤ_» :
Lean.TrailingParserDescr

Uniform isomorphism between `α` and `β`

Equations

- «term_≃ᵤ_» = Lean.ParserDescr.trailingNode `«term_≃ᵤ_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ᵤ ") (Lean.ParserDescr.cat `term 26))

Instances For

source
theorem UniformEquiv.toEquiv_injective {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] :
Function.Injective toEquiv
source
instance UniformEquiv.instEquivLike {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] :
EquivLike (α ≃ᵤ β) α β
Equations

- UniformEquiv.instEquivLike = { coe := fun (h : α ≃ᵤ β) => ⇑h.toEquiv, inv := fun (h : α ≃ᵤ β) => ⇑h.symm, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

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

Inverse of a uniform isomorphism.

Equations

- h.symm = { toEquiv := h.symm, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
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

- UniformEquiv.Simps.apply h = ⇑h

Instances For

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

See Note [custom simps projection]

Equations

- UniformEquiv.Simps.symm_apply h = ⇑h.symm

Instances For

source
@[simp]
theorem UniformEquiv.coe_toEquiv {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
⇑h.toEquiv = ⇑h
source
@[simp]
theorem UniformEquiv.coe_symm_toEquiv {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
⇑h.symm = ⇑h.symm
source
theorem UniformEquiv.ext {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] {h h' : α ≃ᵤ β} (H : ∀ (x : α), h x = h' x) :
h = h'
source
theorem UniformEquiv.ext_iff {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] {h h' : α ≃ᵤ β} :
h = h' ↔ ∀ (x : α), h x = h' x
source
def UniformEquiv.refl (α : Type u_4) [UniformSpace α] :
α ≃ᵤ α

Identity map as a uniform isomorphism.

Equations

- UniformEquiv.refl α = { toEquiv := Equiv.refl α, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
@[simp]
theorem UniformEquiv.refl_apply (α : Type u_4) [UniformSpace α] :
⇑(UniformEquiv.refl α) = id
source
def UniformEquiv.trans {α : Type u} {β : Type u_1} {γ : Type u_2} [UniformSpace α] [UniformSpace β] [UniformSpace γ] (h₁ : α ≃ᵤ β) (h₂ : β ≃ᵤ γ) :
α ≃ᵤ γ

Composition of two uniform isomorphisms.

Equations

- h₁.trans h₂ = { toEquiv := h₁.trans h₂.toEquiv, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
@[simp]
theorem UniformEquiv.trans_apply {α : Type u} {β : Type u_1} {γ : Type u_2} [UniformSpace α] [UniformSpace β] [UniformSpace γ] (h₁ : α ≃ᵤ β) (h₂ : β ≃ᵤ γ) (a : α) :
(h₁.trans h₂) a = h₂ (h₁ a)
source
@[simp]
theorem UniformEquiv.uniformEquiv_mk_coe_symm {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (a : α ≃ β) (b : UniformContinuous a.toFun) (c : UniformContinuous a.invFun) :
⇑{ toEquiv := a, uniformContinuous_toFun := b, uniformContinuous_invFun := c }.symm = ⇑a.symm
source
@[simp]
theorem UniformEquiv.refl_symm {α : Type u} [UniformSpace α] :
(UniformEquiv.refl α).symm = UniformEquiv.refl α
source
theorem UniformEquiv.uniformContinuous {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
UniformContinuous ⇑h
source
theorem UniformEquiv.continuous {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
Continuous ⇑h
source
theorem UniformEquiv.uniformContinuous_symm {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
UniformContinuous ⇑h.symm
source
theorem UniformEquiv.continuous_symm {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
Continuous ⇑h.symm
source
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 := ⋯ }

Instances For

source
theorem UniformEquiv.toHomeomorph_apply {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (e : α ≃ᵤ β) :
⇑e.toHomeomorph = ⇑e
source
theorem UniformEquiv.toHomeomorph_symm_apply {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (e : α ≃ᵤ β) :
⇑e.toHomeomorph.symm = ⇑e.symm
source
@[simp]
theorem UniformEquiv.apply_symm_apply {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) (x : β) :
h (h.symm x) = x
source
@[simp]
theorem UniformEquiv.symm_apply_apply {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) (x : α) :
h.symm (h x) = x
source
theorem UniformEquiv.bijective {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
Function.Bijective ⇑h
source
theorem UniformEquiv.injective {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
Function.Injective ⇑h
source
theorem UniformEquiv.surjective {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
Function.Surjective ⇑h
source
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`.

Equations

- f.changeInv g hg = { toFun := ⇑f, invFun := g, left_inv := ⋯, right_inv := ⋯, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
@[simp]
theorem UniformEquiv.symm_comp_self {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
⇑h.symm ∘ ⇑h = id
source
@[simp]
theorem UniformEquiv.self_comp_symm {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
⇑h ∘ ⇑h.symm = id
source
theorem UniformEquiv.range_coe {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
Set.range ⇑h = Set.univ
source
theorem UniformEquiv.image_symm {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
Set.image ⇑h.symm = Set.preimage ⇑h
source
theorem UniformEquiv.preimage_symm {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
Set.preimage ⇑h.symm = Set.image ⇑h
source
@[simp]
theorem UniformEquiv.image_preimage {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) (s : Set β) :
⇑h '' (⇑h ⁻¹' s) = s
source
@[simp]
theorem UniformEquiv.preimage_image {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) (s : Set α) :
⇑h ⁻¹' (⇑h '' s) = s
source
theorem UniformEquiv.isUniformInducing {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
IsUniformInducing ⇑h
source
theorem UniformEquiv.comap_eq {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
UniformSpace.comap (⇑h) inst✝ = inst✝¹
source
theorem UniformEquiv.isUniformEmbedding {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
IsUniformEmbedding ⇑h
source
theorem UniformEquiv.completeSpace_iff {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (h : α ≃ᵤ β) :
CompleteSpace α ↔ CompleteSpace β
source
noncomputable def UniformEquiv.ofIsUniformEmbedding {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] (f : α → β) (hf : IsUniformEmbedding f) :
α ≃ᵤ ↑(Set.range f)

Uniform equiv given a uniform embedding.

Equations

- UniformEquiv.ofIsUniformEmbedding f hf = { toEquiv := Equiv.ofInjective f ⋯, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

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

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

Equations

- UniformEquiv.setCongr h = { toEquiv := Equiv.setCongr h, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
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.

Equations

- h₁.prodCongr h₂ = { toEquiv := h₁.prodCongr h₂.toEquiv, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
@[simp]
theorem UniformEquiv.prodCongr_symm {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} [UniformSpace α] [UniformSpace β] [UniformSpace γ] [UniformSpace δ] (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) :
(h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm
source
@[simp]
theorem UniformEquiv.coe_prodCongr {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} [UniformSpace α] [UniformSpace β] [UniformSpace γ] [UniformSpace δ] (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) :
⇑(h₁.prodCongr h₂) = Prod.map ⇑h₁ ⇑h₂
source
def UniformEquiv.prodComm (α : Type u) (β : Type u_1) [UniformSpace α] [UniformSpace β] :
α × β ≃ᵤ β × α

`α × β` is uniformly isomorphic to `β × α`.

Equations

- UniformEquiv.prodComm α β = { toEquiv := Equiv.prodComm α β, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
@[simp]
theorem UniformEquiv.prodComm_symm (α : Type u) (β : Type u_1) [UniformSpace α] [UniformSpace β] :
(prodComm α β).symm = prodComm β α
source
@[simp]
theorem UniformEquiv.coe_prodComm (α : Type u) (β : Type u_1) [UniformSpace α] [UniformSpace β] :
⇑(prodComm α β) = Prod.swap
source
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 := ⋯ }

Instances For

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

`α × {*}` is uniformly isomorphic to `α`.

Equations

- UniformEquiv.prodPunit α = { toEquiv := Equiv.prodPUnit α, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
@[simp]
theorem UniformEquiv.prodPunit_apply (α : Type u) [UniformSpace α] :
⇑(prodPunit α) = fun (p : α × PUnit.{u_4 + 1}) => p.1
source
def UniformEquiv.punitProd (α : Type u) [UniformSpace α] :
PUnit.{u_4 + 1} × α ≃ᵤ α

`{*} × α` is uniformly isomorphic to `α`.

Equations

- UniformEquiv.punitProd α = (UniformEquiv.prodComm PUnit.{?u.10 + 1} α).trans (UniformEquiv.prodPunit α)

Instances For

source
@[simp]
theorem UniformEquiv.coe_punitProd (α : Type u) [UniformSpace α] :
⇑(punitProd α) = Prod.snd
source
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

- UniformEquiv.piCongrLeft e = { toEquiv := Equiv.piCongrLeft β e, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
@[simp]
theorem UniformEquiv.piCongrLeft_toEquiv {ι : Type u_4} {ι' : Type u_5} {β : ι' → Type u_6} [(j : ι') → UniformSpace (β j)] (e : ι ≃ ι') :
(piCongrLeft e).toEquiv = Equiv.piCongrLeft β e
source
theorem UniformEquiv.piCongrLeft_apply {ι : Type u_4} {ι' : Type u_5} {β : ι' → Type u_6} [(j : ι') → UniformSpace (β j)] (e : ι ≃ ι') (a✝ : (b : ι) → β (e.symm.symm b)) (a : ι') :
(piCongrLeft e) a✝ a = (Equiv.piCongrLeft' β e.symm).symm a✝ a
source
@[simp]
theorem UniformEquiv.piCongrLeft_refl {ι : Type u_4} {X : ι → Type u_5} [(i : ι) → UniformSpace (X i)] :
piCongrLeft (Equiv.refl ι) = UniformEquiv.refl ((i : ι) → X i)
source
@[simp]
theorem UniformEquiv.piCongrLeft_symm_apply {ι : Type u_4} {ι' : Type u_5} {X : ι' → Type u_6} [(j : ι') → UniformSpace (X j)] (e : ι ≃ ι') :
⇑(piCongrLeft e).symm = fun (x1 : (j : ι') → X j) (x2 : ι) => x1 (e x2)
source
@[simp]
theorem UniformEquiv.piCongrLeft_apply_apply {ι : Type u_4} {ι' : Type u_5} {X : ι' → Type u_6} [(j : ι') → UniformSpace (X j)] (e : ι ≃ ι') (x : (i : ι) → X (e i)) (i : ι) :
(piCongrLeft e) x (e i) = x i
source
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

- UniformEquiv.piCongrRight F = { toEquiv := Equiv.piCongrRight fun (i : ι) => (F i).toEquiv, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
@[simp]
theorem UniformEquiv.piCongrRight_toEquiv {ι : Type u_4} {β₁ : ι → Type u_5} {β₂ : ι → Type u_6} [(i : ι) → UniformSpace (β₁ i)] [(i : ι) → UniformSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ᵤ β₂ i) :
(piCongrRight F).toEquiv = Equiv.piCongrRight fun (i : ι) => (F i).toEquiv
source
@[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 : ι) :
(piCongrRight F) a✝ i = (F i) (a✝ i)
source
@[simp]
theorem UniformEquiv.piCongrRight_symm {ι : Type u_4} {β₁ : ι → Type u_5} {β₂ : ι → Type u_6} [(i : ι) → UniformSpace (β₁ i)] [(i : ι) → UniformSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ᵤ β₂ i) :
(piCongrRight F).symm = piCongrRight fun (i : ι) => (F i).symm
source
@[simp]
theorem UniformEquiv.piCongrRight_refl {ι : Type u_4} {X : ι → Type u_5} [(i : ι) → UniformSpace (X i)] :
(piCongrRight fun (i : ι) => UniformEquiv.refl (X i)) = UniformEquiv.refl ((i : ι) → X i)
source
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

- UniformEquiv.piCongr e F = (UniformEquiv.piCongrRight F).trans (UniformEquiv.piCongrLeft e)

Instances For

source
@[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)
source
@[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₂ : ι₂) :
(piCongr e F) a✝ i₂ = (Equiv.piCongrLeft β₂ e) ((Equiv.piCongrRight fun (i : ι₁) => (F i).toEquiv) a✝) i₂
source
def UniformEquiv.ulift (α : Type u) [UniformSpace α] :
ULift.{v, u} α ≃ᵤ α

Uniform equivalence between `ULift α` and `α`.

Equations

- UniformEquiv.ulift α = { toEquiv := Equiv.ulift, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

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

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

Equations

- UniformEquiv.funUnique ι α = { toEquiv := Equiv.funUnique ι α, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
@[simp]
theorem UniformEquiv.funUnique_symm_apply (ι : Type u_4) (α : Type u_5) [Unique ι] [UniformSpace α] :
⇑(funUnique ι α).symm = uniqueElim
source
@[simp]
theorem UniformEquiv.funUnique_apply (ι : Type u_4) (α : Type u_5) [Unique ι] [UniformSpace α] :
⇑(funUnique ι α) = fun (f : ι → α) => f default
source
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`.

Equations

- UniformEquiv.piFinTwo α = { toEquiv := piFinTwoEquiv α, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
@[simp]
theorem UniformEquiv.piFinTwo_apply (α : Fin 2 → Type u) [(i : Fin 2) → UniformSpace (α i)] :
⇑(piFinTwo α) = fun (f : (i : Fin 2) → α i) => (f 0, f 1)
source
@[simp]
theorem UniformEquiv.piFinTwo_symm_apply (α : Fin 2 → Type u) [(i : Fin 2) → UniformSpace (α i)] :
⇑(piFinTwo α).symm = fun (p : α 0 × α 1) => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
source
def UniformEquiv.finTwoArrow (α : Type u_4) [UniformSpace α] :
(Fin 2 → α) ≃ᵤ α × α

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

Equations

- UniformEquiv.finTwoArrow α = { toEquiv := finTwoArrowEquiv α, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
@[simp]
theorem UniformEquiv.finTwoArrow_apply (α : Type u_4) [UniformSpace α] :
⇑(finTwoArrow α) = fun (f : Fin 2 → α) => (f 0, f 1)
source
@[simp]
theorem UniformEquiv.finTwoArrow_symm_apply (α : Type u_4) [UniformSpace α] :
⇑(finTwoArrow α).symm = fun (x : α × α) => ![x.1, x.2]
source
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.

Equations

- e.image s = { toEquiv := e.image s, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
def UniformEquiv.subtype {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] {p : α → Prop} {q : β → Prop} (e : α ≃ᵤ β) (h : ∀ (a : α), p a ↔ q (e a)) :
{ a : α // p a } ≃ᵤ { b : β // q b }

A uniform isomorphism `e : α ≃ᵤ β` lifts to subtypes `{ a : α // p a } ≃ᵤ { b : β // q b }` provided `p = q ∘ e`.

Equations

- e.subtype h = { toEquiv := e.subtypeEquiv h, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
@[simp]
theorem UniformEquiv.subtype_apply_coe {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] {p : α → Prop} {q : β → Prop} (e : α ≃ᵤ β) (h : ∀ (a : α), p a ↔ q (e a)) (a : { a : α // p a }) :
↑((e.subtype h) a) = e ↑a
source
@[simp]
theorem UniformEquiv.subtype_symm_apply_coe {α : Type u} {β : Type u_1} [UniformSpace α] [UniformSpace β] {p : α → Prop} {q : β → Prop} (e : α ≃ᵤ β) (h : ∀ (a : α), p a ↔ q (e a)) (b : { b : β // q b }) :
↑((e.subtype h).symm b) = e.symm ↑b
source
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 := ⋯ }

Instances For