isDenseEmbedding_val — Mathlib

English

Let α be a topological space and s a dense subset of α. Then the inclusion map i: s → α is a dense embedding (an embedding with dense image).

Русский

Пусть α — топологическое пространство, s ⊆ α плотна в α. Тогда включение i: s → α является плотным вложением (вложение с плотным образом изображения).

LaTeX

$$$$DenseEmbedding(\iota)$$$$

Lean4

theorem isDenseEmbedding_val [TopologicalSpace α] {s : Set α} (hs : Dense s) : IsDenseEmbedding ((↑) : s → α) :=
  { IsEmbedding.subtypeVal with dense := hs.denseRange_val }

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