Icc_mem_nhds

Mathlib.Topology.Instances.ENNReal.Lemmas

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

English

For any x with NeZero x, the left-neighborhood within (−∞, x) is nontrivial.

Русский

Для любого x с NeZero x левая окрестность внутри (−∞, x) не тривиальна.

LaTeX

$$$(nhdsWithin\, x\, (Set.Iio x)).NeBot$ for NeZero x$$

Lean4

theorem Icc_mem_nhds (xt : x ≠ ∞) (ε0 : ε ≠ 0) : Icc (x - ε) (x + ε) ∈ 𝓝 x :=
  (hasBasis_nhds_of_ne_top' xt).mem_of_mem ε0

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

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

Разделы

Аффилиация

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