Theorems · Definition · general topology

DenseRange

{X : Type u} → [TopologicalSpace X] → {α : Type u_1} → (α → X) → Prop

f : α → X has dense range if its range (image) is a dense subset of X.

Defined in

Mathlib.Topology.Defs.Basic

Cited by

164 results in Mathlib

Foundations

Depth 8 from the axioms, rests on 24 definitions · uses no axioms

Assumes

TopologicalSpace