nhdsWithin_neBot — Mathlib

English

If f has dense range, then for every x, nhdsWithin (range f) x is nonempty.

Русский

Если образ f плотно заполнен, то для каждого x окрестности внутри range f непусты.

LaTeX

$$$$ \\text{DenseRange}(f) \\Rightarrow \\forall x, (\\\\nhdsWithin x \\\\mathrm{range}(f)).NeBot. $$$$

Lean4

theorem nhdsWithin_neBot {ι : Type*} {f : ι → α} (h : DenseRange f) (x : α) : NeBot (𝓝[range f] x) :=
  mem_closure_iff_clusterPt.1 (h x)

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