English
If g and f both have dense ranges and g is continuous, then the composition g ∘ f has dense range.
Русский
Если у g и f плотные диапазоны и g непрерывна, то композиция g ∘ f имеет плотный диапазон.
LaTeX
$$$\\text{DenseRange}(g) \\to \\text{DenseRange}(f) \\to \\text{Continuous}(g) \\Rightarrow \\text{DenseRange}(g \\circ f)$$$
Lean4
/-- Composition of a continuous map with dense range and a function with dense range has dense
range. -/
theorem comp {g : Y → Z} {f : α → Y} (hg : DenseRange g) (hf : DenseRange f) (cg : Continuous g) : DenseRange (g ∘ f) :=
by
rw [DenseRange, range_comp]
exact hg.dense_image cg hf
