isUniformEmbedding_coe — Mathlib

English

If α is a T0-space, the inclusion i: α → Completion α is a uniform embedding.

Русский

Пусть α — T0-пространство; включение i: α → Completion α является равномерной вложенностью.

LaTeX

$$$\\text{IsUniformEmbedding}(\\iota:\\alpha \\to \\mathrm{Completion}(\\alpha))$$$

Lean4

theorem isUniformEmbedding_coe [T0Space α] : IsUniformEmbedding ((↑) : α → Completion α) :=
  { comap_uniformity := comap_coe_eq_uniformity α
    injective := separated_pureCauchy_injective }

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