mathlib3 documentation

topology.uniform_space.equiv

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 #

@[nolint]
structure uniform_equiv (α : Type u_4) (β : Type u_5) [uniform_space α] [uniform_space β] :
Type (max u_4 u_5)

Uniform isomorphism between α and β

Instances for uniform_equiv
@[protected, instance]
def uniform_equiv.has_coe_to_fun {α : Type u} {β : Type u_1} [uniform_space α] [uniform_space β] :
has_coe_to_fun ≃ᵤ β) (λ (_x : α ≃ᵤ β), α β)
Equations
@[protected]
def uniform_equiv.symm {α : Type u} {β : Type u_1} [uniform_space α] [uniform_space β] (h : α ≃ᵤ β) :
β ≃ᵤ α

Inverse of a uniform isomorphism.

Equations
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
@[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 : α ≃ᵤ β) :
@[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]
def uniform_equiv.refl (α : Type u_1) [uniform_space α] :
α ≃ᵤ α

Identity map as a uniform isomorphism.

Equations
@[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
@[simp]
theorem uniform_equiv.trans_apply {α : Type u} {β : Type u_1} {γ : Type u_2} [uniform_space α] [uniform_space β] [uniform_space γ] (h₁ : α ≃ᵤ β) (h₂ : β ≃ᵤ γ) (a : α) :
(h₁.trans h₂) a = h₂ (h₁ a)
@[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]
@[protected, continuity]
theorem uniform_equiv.continuous_symm {α : Type u} {β : Type u_1} [uniform_space α] [uniform_space β] (h : α ≃ᵤ β) :
@[simp]
theorem uniform_equiv.to_homeomorph_apply {α : Type u} {β : Type u_1} [uniform_space α] [uniform_space β] (e : α ≃ᵤ β) (ᾰ : α) :
@[protected]
def uniform_equiv.to_homeomorph {α : Type u} {β : Type u_1} [uniform_space α] [uniform_space β] (e : α ≃ᵤ β) :
α ≃ₜ β

A uniform isomorphism as a homeomorphism.

Equations
@[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 : β) :
h ((h.symm) x) = x
@[simp]
theorem uniform_equiv.symm_apply_apply {α : Type u} {β : Type u_1} [uniform_space α] [uniform_space β] (h : α ≃ᵤ β) (x : α) :
(h.symm) (h x) = 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
@[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 β) :
h '' (h ⁻¹' s) = s
@[simp]
theorem uniform_equiv.preimage_image {α : Type u} {β : Type u_1} [uniform_space α] [uniform_space β] (h : α ≃ᵤ β) (s : set α) :
h ⁻¹' (h '' s) = s
@[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
def uniform_equiv.set_congr {α : Type u} [uniform_space α] {s t : set α} (h : s = t) :

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

Equations
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
@[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₂ : γ ≃ᵤ δ) :
(h₁.prod_congr h₂) = prod.map h₁ h₂
def uniform_equiv.prod_comm (α : Type u) (β : Type u_1) [uniform_space α] [uniform_space β] :
α × β ≃ᵤ β × α

α × β is uniformly isomorphic to β × α.

Equations
def uniform_equiv.prod_assoc (α : Type u) (β : Type u_1) (γ : Type u_2) [uniform_space α] [uniform_space β] [uniform_space γ] :
× β) × γ ≃ᵤ α × β × γ

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

Equations

α × {*} is uniformly isomorphic to α.

Equations

{*} × α is uniformly isomorphic to α.

Equations
def uniform_equiv.ulift (α : Type u) [uniform_space α] :

Uniform equivalence between ulift α and α.

Equations
@[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
def uniform_equiv.fun_unique (ι : Type u_1) (α : Type u_2) [unique ι] [uniform_space α] :
α) ≃ᵤ α

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

Equations
def uniform_equiv.pi_fin_two (α : fin 2 Type u) [Π (i : fin 2), uniform_space (α i)] :
(Π (i : fin 2), α i) ≃ᵤ α 0 × α 1

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)] :
@[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)
def uniform_equiv.fin_two_arrow {α : Type u} [uniform_space α] :
(fin 2 α) ≃ᵤ α × α

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
@[simp]
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
@[simp]
theorem equiv.to_uniform_equiv_of_uniform_inducing_apply {α : Type u} {β : Type u_1} [uniform_space α] [uniform_space β] (f : α β) (hf : uniform_inducing f) (ᾰ : α) :