denseRange_inclusion_iff — Mathlib

English

Let s ⊆ t be subsets of a topological space X. The inclusion map from s into t has dense range if and only if t is contained in the closure of s in X.

Русский

Пусть S ⊆ T ⊆ X — подмножества топологического пространства X. Вложение S в T имеет плотное образе тогда и только если T ⊆ cl_X(S).

LaTeX

$$$DenseRange(\\mathrm{inclusion}(s \\subseteq t)) \\iff t \\subseteq \\overline{s}$$$

Lean4

@[simp]
theorem denseRange_inclusion_iff {s t : Set X} (hst : s ⊆ t) : DenseRange (inclusion hst) ↔ t ⊆ closure s := by
  rw [DenseRange, Subtype.dense_iff, ← range_comp, val_comp_inclusion, Subtype.range_coe]

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