quotient — Mathlib

English

The image of a dense set under the quotient map is dense in the quotient space.

Русский

Образ плотной множества через факторное отображение плотно в факторпространстве.

LaTeX

$$$ \\text{Dense}(s) \\Rightarrow \\text{Dense}( \\mathrm{Quotient.mk}' '' s ). $$$

Lean4

/-- The image of a dense set under `Quotient.mk'` is a dense set. -/
theorem quotient [Setoid X] [TopologicalSpace X] {s : Set X} (H : Dense s) : Dense (Quotient.mk' '' s) :=
  Quotient.mk''_surjective.denseRange.dense_image continuous_coinduced_rng H

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