Theorems · Theorem · general topology

DenseRange.comp

∀ {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z] {α : Type u_4} {g : Y → Z}
  {f : α → Y}, DenseRange g → DenseRange f → Continuous g → DenseRange (g ∘ f)

Composition of a continuous map with dense range and a function with dense range has dense range.

Defined in

Mathlib.Topology.Continuous

Cited by

9 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace