English
Let f: β → α be a map with dense range in a metric space α. Then for every x ∈ α and every ε > 0 there exists y ∈ β such that the distance between x and f(y) is less than ε; i.e., x is arbitrarily well approximated by points in the image of f.
Русский
Пусть f: β → α имеет плотный образ в метрическом пространстве α. Тогда для любого x ∈ α и любого ε > 0 существует y ∈ β, такое что d(x, f(y)) < ε; то есть x можно приближать произвольной точкой из образа f.
LaTeX
$$$\\forall x \\in \\alpha \\; \\forall \\varepsilon > 0 \\,\\exists y \\in \\beta \\text{ such that } \\operatorname{dist}(x, f(y)) < \\varepsilon$, если $\\operatorname{DenseRange}(f)$.$$
Lean4
nonrec theorem _root_.DenseRange.exists_dist_lt {β : Type*} {f : β → α} (hf : DenseRange f) (x : α) {ε : ℝ}
(hε : 0 < ε) : ∃ y, dist x (f y) < ε :=
exists_range_iff.1 (hf.exists_dist_lt x hε)
