quotient — Mathlib

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

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