dense_preimage_iff — Mathlib

English

If f is an open quotient map, then Dense (f⁻¹' s) ↔ Dense s for any set s.

Русский

Если f — открытое факторное отображение, тогда плотность предобраза равна плотности образа: Dense (f⁻¹' s) ⇔ Dense s.

LaTeX

$$$\mathrm{Dense}(f^{-1}'s) \leftrightarrow \mathrm{Dense}(s)$ for IsOpenQuotientMap f$$

Lean4

theorem dense_preimage_iff (h : IsOpenQuotientMap f) {s : Set Y} : Dense (f ⁻¹' s) ↔ Dense s :=
  ⟨fun hs ↦ h.surjective.denseRange.dense_of_mapsTo h.continuous hs (mapsTo_preimage _ _), fun hs ↦
    hs.preimage h.isOpenMap⟩

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