isDenseEmbedding_coe — Mathlib

English

The embedding i: α → Completion α is a dense embedding (dense and inducing).

Русский

Вложение i: α → Completion α является плотным вложением (плотное и индуцирующее).

LaTeX

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

Lean4

theorem isDenseEmbedding_coe [T0Space α] : IsDenseEmbedding ((↑) : α → Completion α) :=
  { isDenseInducing_coe with injective := separated_pureCauchy_injective }

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