Mathlib.Topology.UniformSpace.Equiv

UniformEquiv structure

(α : Type*) (β : Type*) [UniformSpace α] [UniformSpace β] extends
  α ≃ β

Full source

/-- Uniform isomorphism between `α` and `β` -/
structure UniformEquiv (α : Type*) (β : Type*) [UniformSpace α] [UniformSpace β] extends
  α ≃ β where
  /-- Uniform continuity of the function -/
  uniformContinuous_toFun : UniformContinuous toFun
  /-- Uniform continuity of the inverse -/
  uniformContinuous_invFun : UniformContinuous invFun

Uniform isomorphism

Informal description

A uniform isomorphism between two uniform spaces $\alpha$ and $\beta$ is a bijection $f : \alpha \to \beta$ such that both $f$ and its inverse $f^{-1}$ are uniformly continuous. This structure extends the notion of a bijective equivalence ($\alpha \simeq \beta$) by adding the uniform continuity conditions.

term_≃ᵤ_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Uniform isomorphism between `α` and `β` -/
infixl:25 " ≃ᵤ " => UniformEquiv

Uniform isomorphism notation

Informal description

The notation `α ≃ᵤ β` denotes a uniform isomorphism between uniform spaces `α` and `β`, which is a bijection with both the function and its inverse being uniformly continuous.

UniformEquiv.toEquiv_injective theorem

: Function.Injective (toEquiv : α ≃ᵤ β → α ≃ β)

Full source

theorem toEquiv_injective : Function.Injective (toEquiv : α ≃ᵤ β → α ≃ β)
  | ⟨e, h₁, h₂⟩, ⟨e', h₁', h₂'⟩, h => by simpa only [mk.injEq]

Injectivity of Uniform Isomorphism to Bijection Map

Informal description

The function that extracts the underlying bijection from a uniform isomorphism is injective. That is, if two uniform isomorphisms between uniform spaces $\alpha$ and $\beta$ have the same underlying bijection, then they must be the same uniform isomorphism.

UniformEquiv.instEquivLike instance

: EquivLike (α ≃ᵤ β) α β

Full source

instance : EquivLike (α ≃ᵤ β) α β where
  coe h := h.toEquiv
  inv h := h.toEquiv.symm
  left_inv h := h.left_inv
  right_inv h := h.right_inv
  coe_injective' _ _ H _ := toEquiv_injective <| DFunLike.ext' H

Uniform Isomorphism as Equivalence-like Structure

Informal description

For any uniform spaces $\alpha$ and $\beta$, a uniform isomorphism $\alpha \simeqᵤ \beta$ can be treated as a bijective function-like object from $\alpha$ to $\beta$.

UniformEquiv.uniformEquiv_mk_coe theorem

(a : Equiv α β) (b c) : (UniformEquiv.mk a b c : α → β) = a

Full source

@[simp]
theorem uniformEquiv_mk_coe (a : Equiv α β) (b c) : (UniformEquiv.mk a b c : α → β) = a :=
  rfl

Uniform isomorphism construction preserves underlying function

Informal description

For any equivalence $a : \alpha \simeq \beta$ and any proofs $b$ and $c$, the underlying function of the uniform isomorphism constructed from $a$, $b$, and $c$ is equal to $a$ as a function from $\alpha$ to $\beta$.

UniformEquiv.symm definition

(h : α ≃ᵤ β) : β ≃ᵤ α

Full source

/-- Inverse of a uniform isomorphism. -/
protected def symm (h : α ≃ᵤ β) : β ≃ᵤ α where
  uniformContinuous_toFun := h.uniformContinuous_invFun
  uniformContinuous_invFun := h.uniformContinuous_toFun
  toEquiv := h.toEquiv.symm

Inverse of a uniform isomorphism

Informal description

Given a uniform isomorphism $ h : \alpha \simeqᵤ \beta $, the inverse uniform isomorphism $ h^{-1} : \beta \simeqᵤ \alpha $ is defined by swapping the forward and inverse functions of $ h $, ensuring that $ h^{-1} $ is a bijection with $ h $ as its inverse. The uniform continuity conditions are also swapped, meaning the uniform continuity of $ h $'s forward function becomes the uniform continuity of $ h^{-1} $'s inverse function, and vice versa.

UniformEquiv.Simps.apply definition

(h : α ≃ᵤ β) : α → β

Full source

/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
  because it is a composition of multiple projections. -/
def Simps.apply (h : α ≃ᵤ β) : α → β :=
  h

Uniform isomorphism application function

Informal description

For a uniform isomorphism $ h : \alpha \simeqᵤ \beta $, the function $ h $ maps elements from the uniform space $ \alpha $ to the uniform space $ \beta $.

UniformEquiv.Simps.symm_apply definition

(h : α ≃ᵤ β) : β → α

Full source

/-- See Note [custom simps projection] -/
def Simps.symm_apply (h : α ≃ᵤ β) : β → α :=
  h.symm

Inverse application of a uniform isomorphism

Informal description

For a uniform isomorphism $ h : \alpha \simeqᵤ \beta $, the function $ h^{-1} $ maps elements from the uniform space $ \beta $ back to the uniform space $ \alpha $.

UniformEquiv.coe_toEquiv theorem

(h : α ≃ᵤ β) : ⇑h.toEquiv = h

Full source

@[simp]
theorem coe_toEquiv (h : α ≃ᵤ β) : ⇑h.toEquiv = h :=
  rfl

Uniform isomorphism equivalence function equality

Informal description

For any uniform isomorphism $h : \alpha \simeqᵤ \beta$, the underlying function of the equivalence $h.\text{toEquiv}$ is equal to $h$ itself.

UniformEquiv.coe_symm_toEquiv theorem

(h : α ≃ᵤ β) : ⇑h.toEquiv.symm = h.symm

Full source

@[simp]
theorem coe_symm_toEquiv (h : α ≃ᵤ β) : ⇑h.toEquiv.symm = h.symm :=
  rfl

Inverse of Uniform Isomorphism as Underlying Equivalence

Informal description

For any uniform isomorphism $h : \alpha \simeqᵤ \beta$, the underlying function of the inverse equivalence $h^{-1} : \beta \simeq \alpha$ is equal to the inverse function of $h$.

UniformEquiv.ext theorem

{h h' : α ≃ᵤ β} (H : ∀ x, h x = h' x) : h = h'

Full source

@[ext]
theorem ext {h h' : α ≃ᵤ β} (H : ∀ x, h x = h' x) : h = h' :=
  toEquiv_injective <| Equiv.ext H

Extensionality of Uniform Isomorphisms: Pointwise Equality Implies Equality

Informal description

For any two uniform isomorphisms $h, h' : \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, if $h(x) = h'(x)$ for all $x \in \alpha$, then $h = h'$.

UniformEquiv.refl definition

(α : Type*) [UniformSpace α] : α ≃ᵤ α

Full source

/-- Identity map as a uniform isomorphism. -/
@[simps! -fullyApplied apply]
protected def refl (α : Type*) [UniformSpace α] : α ≃ᵤ α where
  uniformContinuous_toFun := uniformContinuous_id
  uniformContinuous_invFun := uniformContinuous_id
  toEquiv := Equiv.refl α

Identity uniform isomorphism

Informal description

The identity uniform isomorphism on a uniform space $\alpha$, which is the bijection from $\alpha$ to itself given by the identity function, with both the function and its inverse being uniformly continuous.

UniformEquiv.trans definition

(h₁ : α ≃ᵤ β) (h₂ : β ≃ᵤ γ) : α ≃ᵤ γ

Full source

/-- Composition of two uniform isomorphisms. -/
protected def trans (h₁ : α ≃ᵤ β) (h₂ : β ≃ᵤ γ) : α ≃ᵤ γ where
  uniformContinuous_toFun := h₂.uniformContinuous_toFun.comp h₁.uniformContinuous_toFun
  uniformContinuous_invFun := h₁.uniformContinuous_invFun.comp h₂.uniformContinuous_invFun
  toEquiv := Equiv.trans h₁.toEquiv h₂.toEquiv

Composition of uniform isomorphisms

Informal description

Given two uniform isomorphisms $h₁ : α ≃ᵤ β$ and $h₂ : β ≃ᵤ γ$, their composition $h₂ \circ h₁$ forms a uniform isomorphism $α ≃ᵤ γ$, where the uniform continuity of the composition and its inverse are given by the composition of the respective uniform continuities of $h₁$ and $h₂$.

UniformEquiv.trans_apply theorem

(h₁ : α ≃ᵤ β) (h₂ : β ≃ᵤ γ) (a : α) : h₁.trans h₂ a = h₂ (h₁ a)

Full source

@[simp]
theorem trans_apply (h₁ : α ≃ᵤ β) (h₂ : β ≃ᵤ γ) (a : α) : h₁.trans h₂ a = h₂ (h₁ a) :=
  rfl

Composition of Uniform Isomorphisms Preserves Application

Informal description

Given uniform isomorphisms $h₁ : α ≃ᵤ β$ and $h₂ : β ≃ᵤ γ$, and an element $a ∈ α$, the application of the composed uniform isomorphism $h₁.trans\ h₂$ to $a$ equals the application of $h₂$ to the result of applying $h₁$ to $a$, i.e., $(h₁.trans\ h₂)(a) = h₂(h₁(a))$.

UniformEquiv.uniformEquiv_mk_coe_symm theorem

(a : Equiv α β) (b c) : ((UniformEquiv.mk a b c).symm : β → α) = a.symm

Full source

@[simp]
theorem uniformEquiv_mk_coe_symm (a : Equiv α β) (b c) :
    ((UniformEquiv.mk a b c).symm : β → α) = a.symm :=
  rfl

Inverse of Constructed Uniform Isomorphism Equals Inverse of Underlying Equivalence

Informal description

Given an equivalence $a : \alpha \simeq \beta$ and uniform continuity proofs $b$ and $c$, the underlying function of the inverse of the uniform isomorphism constructed from $a$, $b$, and $c$ is equal to the inverse of the equivalence $a$. That is, for the uniform isomorphism $h := \text{UniformEquiv.mk}(a, b, c)$, we have $h^{-1} = a^{-1}$ as functions from $\beta$ to $\alpha$.

UniformEquiv.refl_symm theorem

: (UniformEquiv.refl α).symm = UniformEquiv.refl α

Full source

@[simp]
theorem refl_symm : (UniformEquiv.refl α).symm = UniformEquiv.refl α :=
  rfl

Inverse of Identity Uniform Isomorphism is Identity

Informal description

The inverse of the identity uniform isomorphism on a uniform space $\alpha$ is itself the identity uniform isomorphism, i.e., $(\text{refl}_\alpha)^{-1} = \text{refl}_\alpha$.

UniformEquiv.uniformContinuous theorem

(h : α ≃ᵤ β) : UniformContinuous h

Full source

protected theorem uniformContinuous (h : α ≃ᵤ β) : UniformContinuous h :=
  h.uniformContinuous_toFun

Uniform continuity of a uniform isomorphism

Informal description

For any uniform isomorphism $h : \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, the map $h : \alpha \to \beta$ is uniformly continuous.

UniformEquiv.continuous theorem

(h : α ≃ᵤ β) : Continuous h

Full source

@[continuity]
protected theorem continuous (h : α ≃ᵤ β) : Continuous h :=
  h.uniformContinuous.continuous

Continuity of Uniform Isomorphisms

Informal description

For any uniform isomorphism $h : \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, the map $h : \alpha \to \beta$ is continuous.

UniformEquiv.uniformContinuous_symm theorem

(h : α ≃ᵤ β) : UniformContinuous h.symm

Full source

protected theorem uniformContinuous_symm (h : α ≃ᵤ β) : UniformContinuous h.symm :=
  h.uniformContinuous_invFun

Uniform continuity of the inverse of a uniform isomorphism

Informal description

For any uniform isomorphism $h : \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, the inverse map $h^{-1} : \beta \to \alpha$ is uniformly continuous.

UniformEquiv.continuous_symm theorem

(h : α ≃ᵤ β) : Continuous h.symm

Full source

@[continuity]
protected theorem continuous_symm (h : α ≃ᵤ β) : Continuous h.symm :=
  h.uniformContinuous_symm.continuous

Continuity of the Inverse of a Uniform Isomorphism

Informal description

For any uniform isomorphism $h : \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, the inverse map $h^{-1} : \beta \to \alpha$ is continuous.

UniformEquiv.toHomeomorph definition

(e : α ≃ᵤ β) : α ≃ₜ β

Full source

/-- A uniform isomorphism as a homeomorphism. -/
protected def toHomeomorph (e : α ≃ᵤ β) : α ≃ₜ β :=
  { e.toEquiv with
    continuous_toFun := e.continuous
    continuous_invFun := e.continuous_symm }

Homeomorphism induced by a uniform isomorphism

Informal description

Given a uniform isomorphism $e : \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, the function `toHomeomorph` constructs a homeomorphism $\alpha \simeqₜ \beta$ from $e$, where the forward and backward maps are continuous (as guaranteed by the uniform continuity of $e$ and its inverse).

UniformEquiv.toHomeomorph_apply theorem

(e : α ≃ᵤ β) : (e.toHomeomorph : α → β) = e

Full source

lemma toHomeomorph_apply (e : α ≃ᵤ β) : (e.toHomeomorph : α → β) = e := rfl

Homeomorphism Induced by Uniform Isomorphism Preserves Mapping

Informal description

For any uniform isomorphism $e : \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, the underlying function of the induced homeomorphism $e.toHomeomorph$ coincides with $e$ itself as a function from $\alpha$ to $\beta$.

UniformEquiv.toHomeomorph_symm_apply theorem

(e : α ≃ᵤ β) : (e.toHomeomorph.symm : β → α) = e.symm

Full source

lemma toHomeomorph_symm_apply (e : α ≃ᵤ β) : (e.toHomeomorph.symm : β → α) = e.symm := rfl

Inverse Homeomorphism of Uniform Isomorphism Equals Inverse Uniform Isomorphism

Informal description

For any uniform isomorphism $e : \alpha \simeqᵤ \beta$, the underlying function of the inverse homeomorphism $e.toHomeomorph.symm : \beta \to \alpha$ is equal to the inverse uniform isomorphism $e.symm : \beta \to \alpha$.

UniformEquiv.apply_symm_apply theorem

(h : α ≃ᵤ β) (x : β) : h (h.symm x) = x

Full source

@[simp]
theorem apply_symm_apply (h : α ≃ᵤ β) (x : β) : h (h.symm x) = x :=
  h.toEquiv.apply_symm_apply x

Uniform Isomorphism Recovery: $h(h^{-1}(x)) = x$

Informal description

For any uniform isomorphism $h : \alpha \simeqᵤ \beta$ and any element $x \in \beta$, applying $h$ to the inverse image $h^{-1}(x)$ recovers the original element $x$, i.e., $h(h^{-1}(x)) = x$.

UniformEquiv.symm_apply_apply theorem

(h : α ≃ᵤ β) (x : α) : h.symm (h x) = x

Full source

@[simp]
theorem symm_apply_apply (h : α ≃ᵤ β) (x : α) : h.symm (h x) = x :=
  h.toEquiv.symm_apply_apply x

Inverse Uniform Isomorphism Recovers Original Element

Informal description

For any uniform isomorphism $h : \alpha \simeqᵤ \beta$ and any element $x \in \alpha$, applying the inverse uniform isomorphism $h^{-1}$ to the image $h(x)$ recovers the original element $x$, i.e., $h^{-1}(h(x)) = x$.

UniformEquiv.bijective theorem

(h : α ≃ᵤ β) : Function.Bijective h

Full source

protected theorem bijective (h : α ≃ᵤ β) : Function.Bijective h :=
  h.toEquiv.bijective

Bijectivity of Uniform Isomorphisms

Informal description

For any uniform isomorphism $h : \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, the function $h : \alpha \to \beta$ is bijective (both injective and surjective).

UniformEquiv.injective theorem

(h : α ≃ᵤ β) : Function.Injective h

Full source

protected theorem injective (h : α ≃ᵤ β) : Function.Injective h :=
  h.toEquiv.injective

Injectivity of Uniform Isomorphisms

Informal description

For any uniform isomorphism $h : \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, the function $h : \alpha \to \beta$ is injective.

UniformEquiv.surjective theorem

(h : α ≃ᵤ β) : Function.Surjective h

Full source

protected theorem surjective (h : α ≃ᵤ β) : Function.Surjective h :=
  h.toEquiv.surjective

Surjectivity of Uniform Isomorphisms

Informal description

For any uniform isomorphism $h : \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, the function $h : \alpha \to \beta$ is surjective.

UniformEquiv.changeInv definition

(f : α ≃ᵤ β) (g : β → α) (hg : Function.RightInverse g f) : α ≃ᵤ β

Full source

/-- Change the uniform equiv `f` to make the inverse function definitionally equal to `g`. -/
def changeInv (f : α ≃ᵤ β) (g : β → α) (hg : Function.RightInverse g f) : α ≃ᵤ β :=
  have : g = f.symm :=
    funext fun x => calc
      g x = f.symm (f (g x)) := (f.left_inv (g x)).symm
      _ = f.symm x := by rw [hg x]
  { toFun := f
    invFun := g
    left_inv := by convert f.left_inv
    right_inv := by convert f.right_inv using 1
    uniformContinuous_toFun := f.uniformContinuous
    uniformContinuous_invFun := by convert f.symm.uniformContinuous }

Uniform isomorphism with specified inverse

Informal description

Given a uniform isomorphism $f : \alpha \simeqᵤ \beta$ and a function $g : \beta \to \alpha$ that is a right inverse of $f$ (i.e., $f \circ g = \text{id}$), this constructs a new uniform isomorphism with the same forward map $f$ but with the inverse map definitionally equal to $g$.

UniformEquiv.symm_comp_self theorem

(h : α ≃ᵤ β) : (h.symm : β → α) ∘ h = id

Full source

@[simp]
theorem symm_comp_self (h : α ≃ᵤ β) : (h.symm : β → α) ∘ h = id :=
  funext h.symm_apply_apply

Inverse Composition Identity for Uniform Isomorphisms

Informal description

For any uniform isomorphism $h \colon \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, the composition of the inverse uniform isomorphism $h^{-1} \colon \beta \to \alpha$ with $h$ is equal to the identity function on $\alpha$, i.e., $h^{-1} \circ h = \text{id}_\alpha$.

UniformEquiv.self_comp_symm theorem

(h : α ≃ᵤ β) : (h : α → β) ∘ h.symm = id

Full source

@[simp]
theorem self_comp_symm (h : α ≃ᵤ β) : (h : α → β) ∘ h.symm = id :=
  funext h.apply_symm_apply

Composition of Uniform Isomorphism with its Inverse Yields Identity

Informal description

For any uniform isomorphism $h \colon \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, the composition of $h$ with its inverse $h^{-1}$ is equal to the identity function on $\beta$, i.e., $h \circ h^{-1} = \text{id}_\beta$.

UniformEquiv.range_coe theorem

(h : α ≃ᵤ β) : range h = univ

Full source

theorem range_coe (h : α ≃ᵤ β) : range h = univ := by simp

Uniform Isomorphisms are Surjective

Informal description

For any uniform isomorphism $h : \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, the range of $h$ is equal to the universal set of $\beta$. In other words, $h$ is surjective.

UniformEquiv.image_symm theorem

(h : α ≃ᵤ β) : image h.symm = preimage h

Full source

theorem image_symm (h : α ≃ᵤ β) : image h.symm = preimage h :=
  funext h.symm.toEquiv.image_eq_preimage

Image under Inverse Uniform Isomorphism Equals Preimage

Informal description

For any uniform isomorphism $h \colon \alpha \simeqᵤ \beta$, the image of a set under the inverse isomorphism $h^{-1}$ is equal to the preimage of the set under $h$, i.e., \[ h^{-1}(S) = h^{-1}(S) \] for any subset $S \subseteq \beta$.

UniformEquiv.preimage_symm theorem

(h : α ≃ᵤ β) : preimage h.symm = image h

Full source

theorem preimage_symm (h : α ≃ᵤ β) : preimage h.symm = image h :=
  (funext h.toEquiv.image_eq_preimage).symm

Preimage under Inverse Uniform Isomorphism Equals Image under Forward Isomorphism

Informal description

For any uniform isomorphism $h \colon \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, the preimage under the inverse isomorphism $h^{-1}$ is equal to the image under $h$. That is, for any subset $s \subseteq \alpha$, \[ h^{-1}{}^{-1}(s) = h(s). \]

UniformEquiv.image_preimage theorem

(h : α ≃ᵤ β) (s : Set β) : h '' (h ⁻¹' s) = s

Full source

@[simp]
theorem image_preimage (h : α ≃ᵤ β) (s : Set β) : h '' (h ⁻¹' s) = s :=
  h.toEquiv.image_preimage s

Image-Preimage Identity for Uniform Isomorphisms

Informal description

For any uniform isomorphism $h : \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, and any subset $s \subseteq \beta$, the image of the preimage of $s$ under $h$ equals $s$ itself. In symbols, $h(h^{-1}(s)) = s$.

UniformEquiv.preimage_image theorem

(h : α ≃ᵤ β) (s : Set α) : h ⁻¹' (h '' s) = s

Full source

@[simp]
theorem preimage_image (h : α ≃ᵤ β) (s : Set α) : h ⁻¹' (h '' s) = s :=
  h.toEquiv.preimage_image s

Preimage of Image under Uniform Isomorphism is Identity

Informal description

For any uniform isomorphism $h : \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, and any subset $s \subseteq \alpha$, the preimage of the image of $s$ under $h$ equals $s$ itself. In symbols, $h^{-1}(h(s)) = s$.

UniformEquiv.isUniformInducing theorem

(h : α ≃ᵤ β) : IsUniformInducing h

Full source

theorem isUniformInducing (h : α ≃ᵤ β) : IsUniformInducing h :=
  IsUniformInducing.of_comp h.uniformContinuous h.symm.uniformContinuous <| by
    simp only [symm_comp_self, IsUniformInducing.id]

Uniform isomorphisms are uniform inducing

Informal description

For any uniform isomorphism $h \colon \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, the map $h$ is a uniform inducing map. That is, the uniformity on $\alpha$ is the pullback of the uniformity on $\beta$ under $h$.

UniformEquiv.comap_eq theorem

(h : α ≃ᵤ β) : UniformSpace.comap h ‹_› = ‹_›

Full source

theorem comap_eq (h : α ≃ᵤ β) : UniformSpace.comap h ‹_› = ‹_› :=
  h.isUniformInducing.comap_uniformSpace

Uniformity Preservation under Uniform Isomorphism

Informal description

For any uniform isomorphism $h \colon \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, the uniformity on $\alpha$ obtained by pulling back the uniformity on $\beta$ via $h$ is equal to the original uniformity on $\alpha$. In other words, $\text{UniformSpace.comap}\, h\,\mathcal{U}_\beta = \mathcal{U}_\alpha$, where $\mathcal{U}_\alpha$ and $\mathcal{U}_\beta$ are the uniformities on $\alpha$ and $\beta$ respectively.

UniformEquiv.isUniformEmbedding theorem

(h : α ≃ᵤ β) : IsUniformEmbedding h

Full source

lemma isUniformEmbedding (h : α ≃ᵤ β) : IsUniformEmbedding h := ⟨h.isUniformInducing, h.injective⟩

Uniform isomorphisms are uniform embeddings

Informal description

For any uniform isomorphism $h \colon \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, the map $h$ is a uniform embedding. That is, $h$ is injective, uniformly continuous, and its inverse (when restricted to the range of $h$) is also uniformly continuous.

UniformEquiv.completeSpace_iff theorem

(h : α ≃ᵤ β) : CompleteSpace α ↔ CompleteSpace β

Full source

theorem completeSpace_iff (h : α ≃ᵤ β) : CompleteSpaceCompleteSpace α ↔ CompleteSpace β :=
  completeSpace_congr h.isUniformEmbedding

Uniform Isomorphism Preserves Completeness: $\text{CompleteSpace}\,\alpha \leftrightarrow \text{CompleteSpace}\,\beta$

Informal description

For any uniform isomorphism $h \colon \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, the space $\alpha$ is complete if and only if $\beta$ is complete.

UniformEquiv.ofIsUniformEmbedding definition

(f : α → β) (hf : IsUniformEmbedding f) : α ≃ᵤ Set.range f

Full source

/-- Uniform equiv given a uniform embedding. -/
noncomputable def ofIsUniformEmbedding (f : α → β) (hf : IsUniformEmbedding f) :
    α ≃ᵤ Set.range f where
  uniformContinuous_toFun := hf.isUniformInducing.uniformContinuous.subtype_mk _
  uniformContinuous_invFun := by
    rw [hf.isUniformInducing.uniformContinuous_iff, Equiv.invFun_as_coe,
      Equiv.self_comp_ofInjective_symm]
    exact uniformContinuous_subtype_val
  toEquiv := Equiv.ofInjective f hf.injective

Uniform isomorphism induced by a uniform embedding

Informal description

Given a function $ f : \alpha \to \beta $ between uniform spaces that is a uniform embedding (i.e., $ f $ is injective and both $ f $ and its inverse when restricted to the range of $ f $ are uniformly continuous), there exists a uniform isomorphism between $ \alpha $ and the range of $ f $. The isomorphism is constructed using the bijection induced by the injectivity of $ f $, and both the forward and inverse maps are uniformly continuous.

UniformEquiv.setCongr definition

{s t : Set α} (h : s = t) : s ≃ᵤ t

Full source

/-- If two sets are equal, then they are uniformly equivalent. -/
def setCongr {s t : Set α} (h : s = t) : s ≃ᵤ t where
  uniformContinuous_toFun := uniformContinuous_subtype_val.subtype_mk _
  uniformContinuous_invFun := uniformContinuous_subtype_val.subtype_mk _
  toEquiv := Equiv.setCongr h

Uniform isomorphism between equal subsets of a uniform space

Informal description

Given two subsets $s$ and $t$ of a uniform space $\alpha$ that are equal ($s = t$), there exists a uniform isomorphism between them. This isomorphism is constructed using the bijection induced by the equality of sets, and both the forward and inverse maps are uniformly continuous when restricted to the subsets.

UniformEquiv.prodCongr definition

(h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) : α × γ ≃ᵤ β × δ

Full source

/-- Product of two uniform isomorphisms. -/
def prodCongr (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) : α × γα × γ ≃ᵤ β × δ where
  uniformContinuous_toFun :=
    (h₁.uniformContinuous.comp uniformContinuous_fst).prodMk
      (h₂.uniformContinuous.comp uniformContinuous_snd)
  uniformContinuous_invFun :=
    (h₁.symm.uniformContinuous.comp uniformContinuous_fst).prodMk
      (h₂.symm.uniformContinuous.comp uniformContinuous_snd)
  toEquiv := h₁.toEquiv.prodCongr h₂.toEquiv

Product of uniform isomorphisms

Informal description

Given uniform isomorphisms $ h₁ : α ≃ᵤ β $ and $ h₂ : γ ≃ᵤ δ $, the product $ h₁.prodCongr h₂ $ is a uniform isomorphism between the product spaces $ α × γ $ and $ β × δ $. The forward map applies $ h₁ $ to the first component and $ h₂ $ to the second component, while the inverse map applies the inverses of $ h₁ $ and $ h₂ $ similarly. Both the forward and inverse maps are uniformly continuous.

UniformEquiv.prodCongr_symm theorem

(h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) : (h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm

Full source

@[simp]
theorem prodCongr_symm (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) :
    (h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm :=
  rfl

Inverse of Product Uniform Isomorphism Equals Product of Inverses

Informal description

Given uniform isomorphisms $h₁ : α ≃ᵤ β$ and $h₂ : γ ≃ᵤ δ$, the inverse of the product uniform isomorphism $h₁.prodCongr h₂$ is equal to the product of the inverses $h₁.symm.prodCongr h₂.symm$. In other words, $(h₁.prodCongr h₂)^{-1} = h₁^{-1}.prodCongr h₂^{-1}$.

UniformEquiv.coe_prodCongr theorem

(h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) : ⇑(h₁.prodCongr h₂) = Prod.map h₁ h₂

Full source

@[simp]
theorem coe_prodCongr (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) : ⇑(h₁.prodCongr h₂) = Prod.map h₁ h₂ :=
  rfl

Product Uniform Isomorphism as Product Map

Informal description

Given uniform isomorphisms $h₁ : α ≃ᵤ β$ and $h₂ : γ ≃ᵤ δ$, the underlying function of the product uniform isomorphism $h₁.prodCongr h₂$ is equal to the product map $\text{Prod.map}\, h₁\, h₂$, which applies $h₁$ to the first component and $h₂$ to the second component of any pair in $α × γ$.

UniformEquiv.prodComm definition

: α × β ≃ᵤ β × α

Full source

/-- `α × β` is uniformly isomorphic to `β × α`. -/
def prodComm : α × βα × β ≃ᵤ β × α where
  uniformContinuous_toFun := uniformContinuous_snd.prodMk uniformContinuous_fst
  uniformContinuous_invFun := uniformContinuous_snd.prodMk uniformContinuous_fst
  toEquiv := Equiv.prodComm α β

Uniform isomorphism between product spaces via swapping

Informal description

The uniform isomorphism between the product spaces $\alpha \times \beta$ and $\beta \times \alpha$ is given by the swap function, which exchanges the two components of a pair. This is a bijection with itself as its own inverse, and both the function and its inverse are uniformly continuous.

UniformEquiv.prodComm_symm theorem

: (prodComm α β).symm = prodComm β α

Full source

@[simp]
theorem prodComm_symm : (prodComm α β).symm = prodComm β α :=
  rfl

Inverse of Product Swap Uniform Isomorphism Equals Swap of Reversed Factors

Informal description

The inverse of the uniform isomorphism swapping the factors of the product space $\alpha \times \beta$ is equal to the uniform isomorphism swapping the factors of $\beta \times \alpha$.

UniformEquiv.coe_prodComm theorem

: ⇑(prodComm α β) = Prod.swap

Full source

@[simp]
theorem coe_prodComm : ⇑(prodComm α β) = Prod.swap :=
  rfl

Uniform isomorphism `prodComm` is implemented by the swap function

Informal description

The underlying function of the uniform isomorphism `prodComm α β` is equal to the swap function `Prod.swap : α × β → β × α`.

UniformEquiv.prodAssoc definition

: (α × β) × γ ≃ᵤ α × β × γ

Full source

/-- `(α × β) × γ` is uniformly isomorphic to `α × (β × γ)`. -/
def prodAssoc : (α × β) × γ(α × β) × γ ≃ᵤ α × β × γ where
  uniformContinuous_toFun :=
    (uniformContinuous_fst.comp uniformContinuous_fst).prodMk
      ((uniformContinuous_snd.comp uniformContinuous_fst).prodMk uniformContinuous_snd)
  uniformContinuous_invFun :=
    (uniformContinuous_fst.prodMk (uniformContinuous_fst.comp
      uniformContinuous_snd)).prodMk (uniformContinuous_snd.comp uniformContinuous_snd)
  toEquiv := Equiv.prodAssoc α β γ

Uniform isomorphism for associativity of products

Informal description

The uniform isomorphism $(α × β) × γ ≃ᵤ α × (β × γ)$ reassociates the components of the product, mapping $((a, b), c)$ to $(a, (b, c))$ and vice versa, with both the forward and inverse maps being uniformly continuous.

UniformEquiv.prodPunit definition

: α × PUnit ≃ᵤ α

Full source

/-- `α × {*}` is uniformly isomorphic to `α`. -/
@[simps! -fullyApplied apply]
def prodPunit : α × PUnitα × PUnit ≃ᵤ α where
  toEquiv := Equiv.prodPUnit α
  uniformContinuous_toFun := uniformContinuous_fst
  uniformContinuous_invFun := uniformContinuous_id.prodMk uniformContinuous_const

Uniform isomorphism between product with unit and base space

Informal description

The uniform isomorphism between the product space $\alpha \times \text{PUnit}$ and $\alpha$, where $\text{PUnit}$ is the unit type with a single element. The isomorphism maps each pair $(a, ())$ to its first component $a$, and its inverse maps each element $a$ of $\alpha$ to the pair $(a, ())$. Both the forward and inverse maps are uniformly continuous.

UniformEquiv.punitProd definition

: PUnit × α ≃ᵤ α

Full source

/-- `{*} × α` is uniformly isomorphic to `α`. -/
def punitProd : PUnitPUnit × αPUnit × α ≃ᵤ α :=
  (prodComm _ _).trans (prodPunit _)

Uniform isomorphism between product with unit in first component and base space

Informal description

The uniform isomorphism between the product space $\text{PUnit} \times \alpha$ and $\alpha$, where $\text{PUnit}$ is the unit type with a single element. The isomorphism maps each pair $((), a)$ to its second component $a$, and its inverse maps each element $a$ of $\alpha$ to the pair $((), a)$. Both the forward and inverse maps are uniformly continuous.

UniformEquiv.coe_punitProd theorem

: ⇑(punitProd α) = Prod.snd

Full source

@[simp]
theorem coe_punitProd : ⇑(punitProd α) = Prod.snd :=
  rfl

Uniform isomorphism `punitProd` equals second projection

Informal description

The underlying function of the uniform isomorphism `punitProd α` from $\text{PUnit} \times \alpha$ to $\alpha$ is equal to the second projection function $\operatorname{snd}$.

UniformEquiv.piCongrLeft definition

 {ι ι' : Type*} {β : ι' → Type*} [∀ j, UniformSpace (β j)] (e : ι ≃ ι') : (∀ i, β (e i)) ≃ᵤ ∀ j, β j

Full source

/-- `Equiv.piCongrLeft` as a uniform isomorphism: this is the natural isomorphism
`Π i, β (e i) ≃ᵤ Π j, β j` obtained from a bijection `ι ≃ ι'`. -/
@[simps! apply toEquiv]
def piCongrLeft {ι ι' : Type*} {β : ι' → Type*} [∀ j, UniformSpace (β j)]
    (e : ι ≃ ι') : (∀ i, β (e i)) ≃ᵤ ∀ j, β j where
  uniformContinuous_toFun := uniformContinuous_pi.mpr <| e.forall_congr_right.mp fun i ↦ by
    simpa only [Equiv.toFun_as_coe, Equiv.piCongrLeft_apply_apply] using
      Pi.uniformContinuous_proj _ i
  uniformContinuous_invFun := Pi.uniformContinuous_precomp' _ e
  toEquiv := Equiv.piCongrLeft _ e

Uniform isomorphism of dependent function spaces under index bijection

Informal description

Given a bijection $e : \iota \simeq \iota'$ between index types and a family of uniform spaces $\beta_j$ indexed by $j \in \iota'$, the uniform isomorphism $\text{UniformEquiv.piCongrLeft}$ constructs a natural isomorphism between the dependent function spaces $\prod_{i \in \iota} \beta_{e(i)}$ and $\prod_{j \in \iota'} \beta_j$. Specifically: - The forward map sends a function $f : \prod_{i \in \iota} \beta_{e(i)}$ to the function $j \mapsto f(e^{-1}j)$. - The inverse map sends a function $g : \prod_{j \in \iota'} \beta_j$ to the function $i \mapsto g(e i)$. Both the forward and inverse maps are uniformly continuous, making this a uniform isomorphism.

UniformEquiv.piCongrRight definition

 {ι : Type*} {β₁ β₂ : ι → Type*} [∀ i, UniformSpace (β₁ i)] [∀ i, UniformSpace (β₂ i)] (F : ∀ i, β₁ i ≃ᵤ β₂ i) :
  (∀ i, β₁ i) ≃ᵤ ∀ i, β₂ i

Full source

/-- `Equiv.piCongrRight` as a uniform isomorphism: this is the natural isomorphism
`Π i, β₁ i ≃ᵤ Π j, β₂ i` obtained from uniform isomorphisms `β₁ i ≃ᵤ β₂ i` for each `i`. -/
@[simps! apply toEquiv]
def piCongrRight {ι : Type*} {β₁ β₂ : ι → Type*} [∀ i, UniformSpace (β₁ i)]
    [∀ i, UniformSpace (β₂ i)] (F : ∀ i, β₁ i ≃ᵤ β₂ i) : (∀ i, β₁ i) ≃ᵤ ∀ i, β₂ i where
  uniformContinuous_toFun := Pi.uniformContinuous_postcomp' _ fun i ↦ (F i).uniformContinuous
  uniformContinuous_invFun := Pi.uniformContinuous_postcomp' _ fun i ↦ (F i).symm.uniformContinuous
  toEquiv := Equiv.piCongrRight fun i => (F i).toEquiv

Uniform isomorphism of dependent function spaces via component-wise uniform isomorphisms

Informal description

Given a family of uniform isomorphisms $ F_i : \beta_1 i \simeq \beta_2 i $ indexed by $ i \in \iota $, where each $ \beta_1 i $ and $ \beta_2 i $ are uniform spaces, the function space $ \prod_{i} \beta_1 i $ is uniformly isomorphic to $ \prod_{i} \beta_2 i $ via component-wise application of each $ F_i $. The uniform continuity of both the forward and inverse maps is ensured by the uniform continuity of each $ F_i $ and their inverses.

UniformEquiv.piCongrRight_symm theorem

 {ι : Type*} {β₁ β₂ : ι → Type*} [∀ i, UniformSpace (β₁ i)] [∀ i, UniformSpace (β₂ i)] (F : ∀ i, β₁ i ≃ᵤ β₂ i) :
  (piCongrRight F).symm = piCongrRight fun i => (F i).symm

Full source

@[simp]
theorem piCongrRight_symm {ι : Type*} {β₁ β₂ : ι → Type*} [∀ i, UniformSpace (β₁ i)]
    [∀ i, UniformSpace (β₂ i)] (F : ∀ i, β₁ i ≃ᵤ β₂ i) :
    (piCongrRight F).symm = piCongrRight fun i => (F i).symm :=
  rfl

Inverse of Component-wise Uniform Isomorphism Equals Component-wise Inverses

Informal description

For any family of uniform isomorphisms $F_i : \beta_1 i \simeq \beta_2 i$ indexed by $i \in \iota$, where each $\beta_1 i$ and $\beta_2 i$ are uniform spaces, the inverse of the uniform isomorphism $\prod_{i} \beta_1 i \simeq \prod_{i} \beta_2 i$ (constructed by component-wise application of $F_i$) is equal to the uniform isomorphism constructed by component-wise application of the inverses $(F_i)^{-1} : \beta_2 i \simeq \beta_1 i$.

UniformEquiv.piCongr definition

 {ι₁ ι₂ : Type*} {β₁ : ι₁ → Type*} {β₂ : ι₂ → Type*} [∀ i₁, UniformSpace (β₁ i₁)] [∀ i₂, UniformSpace (β₂ i₂)]
  (e : ι₁ ≃ ι₂) (F : ∀ i₁, β₁ i₁ ≃ᵤ β₂ (e i₁)) : (∀ i₁, β₁ i₁) ≃ᵤ ∀ i₂, β₂ i₂

Full source

/-- `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₁ : ι₁`. -/
@[simps! apply toEquiv]
def piCongr {ι₁ ι₂ : Type*} {β₁ : ι₁ → Type*} {β₂ : ι₂ → Type*}
    [∀ i₁, UniformSpace (β₁ i₁)] [∀ i₂, UniformSpace (β₂ i₂)]
    (e : ι₁ ≃ ι₂) (F : ∀ i₁, β₁ i₁ ≃ᵤ β₂ (e i₁)) : (∀ i₁, β₁ i₁) ≃ᵤ ∀ i₂, β₂ i₂ :=
  (UniformEquiv.piCongrRight F).trans (UniformEquiv.piCongrLeft e)

Uniform isomorphism of dependent function spaces under index bijection and component-wise uniform isomorphisms

Informal description

Given a bijection $e : \iota_1 \simeq \iota_2$ between index types and a family of uniform isomorphisms $F_{i_1} : \beta_1 i_1 \simeq \beta_2 (e i_1)$ for each $i_1 \in \iota_1$, the uniform isomorphism $\text{UniformEquiv.piCongr}$ constructs a natural isomorphism between the dependent function spaces $\prod_{i_1 \in \iota_1} \beta_1 i_1$ and $\prod_{i_2 \in \iota_2} \beta_2 i_2$. This is achieved by first applying the component-wise uniform isomorphisms $F_{i_1}$ (via $\text{UniformEquiv.piCongrRight}$) and then reindexing the function space using the bijection $e$ (via $\text{UniformEquiv.piCongrLeft}$). Both the forward and inverse maps are uniformly continuous.

UniformEquiv.ulift definition

: ULift.{v, u} α ≃ᵤ α

Full source

/-- Uniform equivalence between `ULift α` and `α`. -/
def ulift : ULiftULift.{v, u} α ≃ᵤ α :=
  { Equiv.ulift with
    uniformContinuous_toFun := uniformContinuous_comap
    uniformContinuous_invFun := by
      have hf : IsUniformInducing (@Equiv.ulift.{v, u} α).toFun := ⟨rfl⟩
      simp_rw [hf.uniformContinuous_iff]
      exact uniformContinuous_id }

Uniform isomorphism between `ULift α` and `α`

Informal description

The uniform isomorphism `UniformEquiv.ulift` establishes a bijection between the type `ULift α` and `α`, where both the lifting function `ULift.up` and the projection function `ULift.down` are uniformly continuous. This means that the equivalence preserves the uniform structure of the spaces involved.

UniformEquiv.funUnique definition

(ι α : Type*) [Unique ι] [UniformSpace α] : (ι → α) ≃ᵤ α

Full source

/-- If `ι` has a unique element, then `ι → α` is uniformly isomorphic to `α`. -/
@[simps! -fullyApplied]
def funUnique (ι α : Type*) [Unique ι] [UniformSpace α] : (ι → α) ≃ᵤ α where
  toEquiv := Equiv.funUnique ι α
  uniformContinuous_toFun := Pi.uniformContinuous_proj _ _
  uniformContinuous_invFun := uniformContinuous_pi.mpr fun _ => uniformContinuous_id

Uniform isomorphism between functions from a singleton type and their codomain

Informal description

Given a type $\iota$ with a unique element and a uniform space $\alpha$, the space of functions from $\iota$ to $\alpha$ is uniformly isomorphic to $\alpha$ itself. The isomorphism maps a function $f$ to its value at the unique element of $\iota$, and conversely, any element $a \in \alpha$ can be viewed as the constant function with value $a$. Both the forward and inverse maps are uniformly continuous.

UniformEquiv.piFinTwo definition

(α : Fin 2 → Type u) [∀ i, UniformSpace (α i)] : (∀ i, α i) ≃ᵤ α 0 × α 1

Full source

/-- Uniform isomorphism between dependent functions `Π i : Fin 2, α i` and `α 0 × α 1`. -/
@[simps! -fullyApplied]
def piFinTwo (α : Fin 2 → Type u) [∀ i, UniformSpace (α i)] : (∀ i, α i) ≃ᵤ α 0 × α 1 where
  toEquiv := piFinTwoEquiv α
  uniformContinuous_toFun := (Pi.uniformContinuous_proj _ 0).prodMk (Pi.uniformContinuous_proj _ 1)
  uniformContinuous_invFun :=
    uniformContinuous_pi.mpr <| Fin.forall_fin_two.2 ⟨uniformContinuous_fst, uniformContinuous_snd⟩

Uniform isomorphism between dependent functions on `Fin 2` and pairs

Informal description

The uniform isomorphism `UniformEquiv.piFinTwo` establishes a bijection between dependent functions on `Fin 2` (i.e., pairs of elements where the first is of type `α 0` and the second is of type `α 1`) and the Cartesian product `α 0 × α 1`, where both the function and its inverse are uniformly continuous. Specifically: - The forward direction maps a function `f : ∀ i : Fin 2, α i` to the pair `(f 0, f 1)`. - The backward direction reconstructs the function from a pair `(x, y)` by prepending `x` and `y` using `Fin.cons`, with the empty case handled by `finZeroElim`.

UniformEquiv.finTwoArrow definition

(α : Type*) [UniformSpace α] : (Fin 2 → α) ≃ᵤ α × α

Full source

/-- Uniform isomorphism between `α² = Fin 2 → α` and `α × α`. -/
@[simps! -fullyApplied]
def finTwoArrow (α : Type*) [UniformSpace α] : (Fin 2 → α) ≃ᵤ α × α :=
  { piFinTwo fun _ => α with toEquiv := finTwoArrowEquiv α }

Uniform isomorphism between functions on `Fin 2` and pairs in `α × α`

Informal description

The uniform isomorphism `UniformEquiv.finTwoArrow` establishes a bijection between the space of functions from `Fin 2` to a uniform space `α` and the Cartesian product `α × α`, where both the function and its inverse are uniformly continuous. Specifically: - The forward direction maps a function `f : Fin 2 → α` to the pair `(f 0, f 1)`. - The backward direction maps a pair `(x, y)` to the function `Fin.cons x (Fin.cons y finZeroElim)`.

UniformEquiv.image definition

(e : α ≃ᵤ β) (s : Set α) : s ≃ᵤ e '' s

Full source

/-- A subset of a uniform space is uniformly isomorphic to its image under a uniform isomorphism.
-/
def image (e : α ≃ᵤ β) (s : Set α) : s ≃ᵤ e '' s where
  uniformContinuous_toFun := (e.uniformContinuous.comp uniformContinuous_subtype_val).subtype_mk _
  uniformContinuous_invFun :=
    (e.symm.uniformContinuous.comp uniformContinuous_subtype_val).subtype_mk _
  toEquiv := e.toEquiv.image s

Uniform isomorphism between a subset and its image under a uniform isomorphism

Informal description

Given a uniform isomorphism $e : \alpha \simeqᵤ \beta$ between uniform spaces $\alpha$ and $\beta$, and a subset $s \subseteq \alpha$, the restriction of $e$ to $s$ is a uniform isomorphism between $s$ and its image $e(s) \subseteq \beta$. This means: 1. The restricted map $e|_s : s \to e(s)$ is uniformly continuous. 2. The inverse map $(e|_s)^{-1} : e(s) \to s$ is also uniformly continuous. 3. The underlying bijection is given by the image equivalence $e(s) \simeq s$ induced by $e$.

Equiv.toUniformEquivOfIsUniformInducing definition

[UniformSpace α] [UniformSpace β] (f : α ≃ β) (hf : IsUniformInducing f) : α ≃ᵤ β

Full source

/-- A uniform inducing equiv between uniform spaces is a uniform isomorphism. -/
def Equiv.toUniformEquivOfIsUniformInducing [UniformSpace α] [UniformSpace β] (f : α ≃ β)
    (hf : IsUniformInducing f) : α ≃ᵤ β :=
  { f with
    uniformContinuous_toFun := hf.uniformContinuous
    uniformContinuous_invFun := hf.uniformContinuous_iff.2 <| by simpa using uniformContinuous_id }

Uniform isomorphism induced by a uniform inducing bijection

Informal description

Given a bijection $f : \alpha \to \beta$ between two uniform spaces $\alpha$ and $\beta$, if $f$ is a uniform inducing map (i.e., the uniformity on $\beta$ is induced by $f$ from the uniformity on $\alpha$), then $f$ can be promoted to a uniform isomorphism $\alpha \simeqᵤ \beta$. This means both $f$ and its inverse $f^{-1}$ are uniformly continuous.

Main definitions