isDenseEmbedding — Mathlib

English

If f is a uniform embedding and has dense range, then f is a dense embedding.

Русский

Если отображение является равномерным вложением и имеет плотное образующее множество, то оно плотное вложение.

LaTeX

$$$\\text{IsUniformEmbedding}(f) \\land \\text{DenseRange}(f) \\Rightarrow \\text{IsDenseEmbedding}(f)$$$

Lean4

theorem isDenseEmbedding {f : α → β} (h : IsUniformEmbedding f) (hd : DenseRange f) : IsDenseEmbedding f :=
  { h.isEmbedding with dense := hd }

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