isUniformEmbedding_comap — Mathlib

English

If f is injective, then the map f: α → β from the comap of a uniform space structure on α is a uniform embedding into β.

Русский

Если f инъективно отображает α в β, то отображение f: α → β из перенесённой равномерной структуры является равномерным вложением.

LaTeX

$$$\text{If } f\text{ is injective, then } f:(\alpha,\text{comap } f(u))\to (\beta,u)\text{ is a uniform embedding.}$$$

Lean4

theorem isUniformEmbedding_comap {α : Type*} {β : Type*} {f : α → β} [u : UniformSpace β] (hf : Function.Injective f) :
    @IsUniformEmbedding α β (UniformSpace.comap f u) u f :=
  @IsUniformEmbedding.mk _ _ (UniformSpace.comap f u) _ _ (@IsUniformInducing.mk _ _ (UniformSpace.comap f u) _ _ rfl)
    hf

Похожие утверждения