nhds_of_ne_top

Mathlib.Topology.Instances.ENNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#ENNReal.nhds_of_ne_top

English

The infimum over ε>0 of the principal filters of Icc(x−ε, x+ε) is below nhds x.

Русский

Вкладение по ε>0 от Icc(x−ε, x+ε) моторит nhds x.

LaTeX

$$$\\iInf_{\\varepsilon>0} \\mathcal{P}(Icc(x-\\varepsilon, x+\\varepsilon)) \\le \\mathcal{N}x$$$

Lean4

theorem nhds_of_ne_top (xt : x ≠ ∞) : 𝓝 x = ⨅ ε > 0, 𝓟 (Icc (x - ε) (x + ε)) :=
  (hasBasis_nhds_of_ne_top xt).eq_biInf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru