nhds_zero — Mathlib

English

The neighborhood filter at 0 in NNReal is described by a particular infimum of principal neighborhoods.

Русский

Соседственный фильтр в нуле NNReal описывается через пересечение базовых окрестностей.

LaTeX

$$$\\mathcal{N}(0) = \\bigwedge_{a\\neq 0} \\mathcal{P}(Iio(a))$$$

Lean4

theorem nhds_zero : 𝓝 (0 : ℝ≥0) = ⨅ (a : ℝ≥0) (_ : a ≠ 0), 𝓟 (Iio a) :=
  nhds_bot_order.trans <| by simp only [bot_lt_iff_ne_bot]; rfl

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