isDenseInducing_val — Mathlib

English

If a subset s of α is dense in α, then the inclusion map s → α is a dense inducing map.

Русский

Если подмножество s плотное в α, то включение s в α является плотным индуциирующим отображением.

LaTeX

$$$ Dense s \\to IsDenseInducing (Subtype.val : s \\to \\alpha)$$$

Lean4

theorem _root_.Dense.isDenseInducing_val {s : Set α} (hs : Dense s) : IsDenseInducing (@Subtype.val α s) :=
  ⟨IsInducing.subtypeVal, hs.denseRange_val⟩

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