Uniform isomorphisms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
uniform_equiv α β: The type of uniform isomorphisms fromαtoβ. This type can be denoted using the following notation:α ≃ᵤ β.
@[nolint]
structure
uniform_equiv
(α : Type u_4)
(β : Type u_5)
[uniform_space α]
[uniform_space β] :
Type (max u_4 u_5)
- to_equiv : α ≃ β
- uniform_continuous_to_fun : uniform_continuous self.to_equiv.to_fun
- uniform_continuous_inv_fun : uniform_continuous self.to_equiv.inv_fun
Uniform isomorphism between α and β
Instances for uniform_equiv
- uniform_equiv.has_sizeof_inst
- uniform_equiv.has_coe_to_fun
@[protected, instance]
def
uniform_equiv.has_coe_to_fun
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β] :
has_coe_to_fun (α ≃ᵤ β) (λ (_x : α ≃ᵤ β), α → β)
@[simp]
theorem
uniform_equiv.uniform_equiv_mk_coe
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(a : α ≃ β)
(b : uniform_continuous a.to_fun)
(c : uniform_continuous a.inv_fun) :
⇑{to_equiv := a, uniform_continuous_to_fun := b, uniform_continuous_inv_fun := c} = ⇑a
@[protected]
def
uniform_equiv.symm
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
β ≃ᵤ α
Inverse of a uniform isomorphism.
Equations
- h.symm = {to_equiv := h.to_equiv.symm, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}
def
uniform_equiv.simps.apply
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(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
uniform_equiv.simps.symm_apply
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
β → α
See Note [custom simps projection]
Equations
@[simp]
theorem
uniform_equiv.coe_to_equiv
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
@[simp]
theorem
uniform_equiv.coe_symm_to_equiv
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
theorem
uniform_equiv.to_equiv_injective
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β] :
@[ext]
theorem
uniform_equiv.ext
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
{h h' : α ≃ᵤ β}
(H : ∀ (x : α), ⇑h x = ⇑h' x) :
h = h'
@[protected]
Identity map as a uniform isomorphism.
Equations
- uniform_equiv.refl α = {to_equiv := equiv.refl α, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}
@[simp]
@[protected]
def
uniform_equiv.trans
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
[uniform_space α]
[uniform_space β]
[uniform_space γ]
(h₁ : α ≃ᵤ β)
(h₂ : β ≃ᵤ γ) :
α ≃ᵤ γ
Composition of two uniform isomorphisms.
Equations
- h₁.trans h₂ = {to_equiv := h₁.to_equiv.trans h₂.to_equiv, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}
@[simp]
theorem
uniform_equiv.trans_apply
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
[uniform_space α]
[uniform_space β]
[uniform_space γ]
(h₁ : α ≃ᵤ β)
(h₂ : β ≃ᵤ γ)
(a : α) :
@[simp]
theorem
uniform_equiv.uniform_equiv_mk_coe_symm
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(a : α ≃ β)
(b : uniform_continuous a.to_fun)
(c : uniform_continuous a.inv_fun) :
⇑({to_equiv := a, uniform_continuous_to_fun := b, uniform_continuous_inv_fun := c}.symm) = ⇑(a.symm)
@[simp]
@[protected]
theorem
uniform_equiv.uniform_continuous
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
@[protected, continuity]
theorem
uniform_equiv.continuous
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
@[protected]
theorem
uniform_equiv.uniform_continuous_symm
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
@[protected, continuity]
theorem
uniform_equiv.continuous_symm
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
continuous ⇑(h.symm)
@[simp]
theorem
uniform_equiv.to_homeomorph_apply
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(e : α ≃ᵤ β)
(ᾰ : α) :
⇑(e.to_homeomorph) ᾰ = e.to_equiv.to_fun ᾰ
@[protected]
def
uniform_equiv.to_homeomorph
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(e : α ≃ᵤ β) :
α ≃ₜ β
A uniform isomorphism as a homeomorphism.
Equations
- e.to_homeomorph = {to_equiv := {to_fun := e.to_equiv.to_fun, inv_fun := e.to_equiv.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
uniform_equiv.to_homeomorph_symm_apply
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(e : α ≃ᵤ β)
(ᾰ : β) :
@[simp]
theorem
uniform_equiv.apply_symm_apply
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β)
(x : β) :
@[simp]
theorem
uniform_equiv.symm_apply_apply
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β)
(x : α) :
@[protected]
theorem
uniform_equiv.bijective
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
@[protected]
theorem
uniform_equiv.injective
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
@[protected]
theorem
uniform_equiv.surjective
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
def
uniform_equiv.change_inv
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(f : α ≃ᵤ β)
(g : β → α)
(hg : function.right_inverse g ⇑f) :
α ≃ᵤ β
Change the uniform equiv f to make the inverse function definitionally equal to g.
Equations
- f.change_inv g hg = have this : g = ⇑(f.symm), from _, {to_equiv := {to_fun := ⇑f, inv_fun := g, left_inv := _, right_inv := _}, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}
@[simp]
theorem
uniform_equiv.symm_comp_self
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
@[simp]
theorem
uniform_equiv.self_comp_symm
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
@[simp]
theorem
uniform_equiv.range_coe
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
theorem
uniform_equiv.image_symm
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
theorem
uniform_equiv.preimage_symm
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
@[simp]
theorem
uniform_equiv.image_preimage
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β)
(s : set β) :
@[simp]
theorem
uniform_equiv.preimage_image
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β)
(s : set α) :
@[protected]
theorem
uniform_equiv.uniform_inducing
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
theorem
uniform_equiv.comap_eq
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
uniform_space.comap ⇑h _inst_2 = _inst_1
@[protected]
theorem
uniform_equiv.uniform_embedding
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(h : α ≃ᵤ β) :
noncomputable
def
uniform_equiv.of_uniform_embedding
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(f : α → β)
(hf : uniform_embedding f) :
Uniform equiv given a uniform embedding.
Equations
- uniform_equiv.of_uniform_embedding f hf = {to_equiv := equiv.of_injective f _, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}
If two sets are equal, then they are uniformly equivalent.
Equations
- uniform_equiv.set_congr h = {to_equiv := equiv.set_congr h, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}
def
uniform_equiv.prod_congr
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
{δ : Type u_3}
[uniform_space α]
[uniform_space β]
[uniform_space γ]
[uniform_space δ]
(h₁ : α ≃ᵤ β)
(h₂ : γ ≃ᵤ δ) :
Product of two uniform isomorphisms.
Equations
- h₁.prod_congr h₂ = {to_equiv := h₁.to_equiv.prod_congr h₂.to_equiv, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}
@[simp]
theorem
uniform_equiv.prod_congr_symm
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
{δ : Type u_3}
[uniform_space α]
[uniform_space β]
[uniform_space γ]
[uniform_space δ]
(h₁ : α ≃ᵤ β)
(h₂ : γ ≃ᵤ δ) :
(h₁.prod_congr h₂).symm = h₁.symm.prod_congr h₂.symm
@[simp]
theorem
uniform_equiv.coe_prod_congr
{α : Type u}
{β : Type u_1}
{γ : Type u_2}
{δ : Type u_3}
[uniform_space α]
[uniform_space β]
[uniform_space γ]
[uniform_space δ]
(h₁ : α ≃ᵤ β)
(h₂ : γ ≃ᵤ δ) :
α × β is uniformly isomorphic to β × α.
Equations
- uniform_equiv.prod_comm α β = {to_equiv := equiv.prod_comm α β, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}
@[simp]
theorem
uniform_equiv.prod_comm_symm
(α : Type u)
(β : Type u_1)
[uniform_space α]
[uniform_space β] :
(uniform_equiv.prod_comm α β).symm = uniform_equiv.prod_comm β α
@[simp]
theorem
uniform_equiv.coe_prod_comm
(α : Type u)
(β : Type u_1)
[uniform_space α]
[uniform_space β] :
def
uniform_equiv.prod_assoc
(α : Type u)
(β : Type u_1)
(γ : Type u_2)
[uniform_space α]
[uniform_space β]
[uniform_space γ] :
(α × β) × γ is uniformly isomorphic to α × (β × γ).
Equations
- uniform_equiv.prod_assoc α β γ = {to_equiv := equiv.prod_assoc α β γ, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}
@[simp]
α × {*} is uniformly isomorphic to α.
Equations
{*} × α is uniformly isomorphic to α.
Equations
@[simp]
Uniform equivalence between ulift α and α.
Equations
- uniform_equiv.ulift α = {to_equiv := {to_fun := equiv.ulift.to_fun, inv_fun := equiv.ulift.inv_fun, left_inv := _, right_inv := _}, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}
@[simp]
theorem
uniform_equiv.fun_unique_symm_apply
(ι : Type u_1)
(α : Type u_2)
[unique ι]
[uniform_space α] :
⇑((uniform_equiv.fun_unique ι α).symm) = λ (x : α) (b : ι), x
@[simp]
If ι has a unique element, then ι → α is homeomorphic to α.
Equations
- uniform_equiv.fun_unique ι α = {to_equiv := equiv.fun_unique ι α _inst_5, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}
Uniform isomorphism between dependent functions Π i : fin 2, α i and α 0 × α 1.
Equations
@[simp]
theorem
uniform_equiv.pi_fin_two_symm_apply
(α : fin 2 → Type u)
[Π (i : fin 2), uniform_space (α i)] :
⇑((uniform_equiv.pi_fin_two α).symm) = λ (p : α 0 × α 1), fin.cons p.fst (fin.cons p.snd fin_zero_elim)
@[simp]
theorem
uniform_equiv.pi_fin_two_apply
(α : fin 2 → Type u)
[Π (i : fin 2), uniform_space (α i)] :
⇑(uniform_equiv.pi_fin_two α) = λ (f : Π (i : fin 2), α i), (f 0, f 1)
@[simp]
Uniform isomorphism between α² = fin 2 → α and α × α.
Equations
@[simp]
theorem
uniform_equiv.fin_two_arrow_apply
{α : Type u}
[uniform_space α] :
⇑uniform_equiv.fin_two_arrow = λ (f : fin 2 → α), (f 0, f 1)
def
uniform_equiv.image
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(e : α ≃ᵤ β)
(s : set α) :
A subset of a uniform space is uniformly isomorphic to its image under a uniform isomorphism.
Equations
- e.image s = {to_equiv := e.to_equiv.image s, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}
@[simp]
theorem
equiv.to_uniform_equiv_of_uniform_inducing_symm_apply
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(f : α ≃ β)
(hf : uniform_inducing ⇑f)
(ᾰ : β) :
⇑((f.to_uniform_equiv_of_uniform_inducing hf).symm) ᾰ = f.inv_fun ᾰ
def
equiv.to_uniform_equiv_of_uniform_inducing
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(f : α ≃ β)
(hf : uniform_inducing ⇑f) :
α ≃ᵤ β
A uniform inducing equiv between uniform spaces is a uniform isomorphism.
Equations
- f.to_uniform_equiv_of_uniform_inducing hf = {to_equiv := {to_fun := f.to_fun, inv_fun := f.inv_fun, left_inv := _, right_inv := _}, uniform_continuous_to_fun := _, uniform_continuous_inv_fun := _}
@[simp]
theorem
equiv.to_uniform_equiv_of_uniform_inducing_apply
{α : Type u}
{β : Type u_1}
[uniform_space α]
[uniform_space β]
(f : α ≃ β)
(hf : uniform_inducing ⇑f)
(ᾰ : α) :
⇑(f.to_uniform_equiv_of_uniform_inducing hf) ᾰ = f.to_fun ᾰ