English
The composition of Quotient.mk' with a function having dense range has dense range.
Русский
Произведение Quotient.mk' и отображения с плотным образом имеет плотный образ.
LaTeX
$$$ \\operatorname{DenseRange}(f) \\Rightarrow \\operatorname{DenseRange}(\\mathrm{Quotient.mk}' \\circ f). $$$
Lean4
/-- The composition of `Quotient.mk'` and a function with dense range has dense range. -/
theorem quotient [Setoid X] [TopologicalSpace X] {f : Y → X} (hf : DenseRange f) : DenseRange (Quotient.mk' ∘ f) :=
Quotient.mk''_surjective.denseRange.comp hf continuous_coinduced_rng