nhds_zero_basis

Mathlib.Topology.Instances.NNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#NNReal.nhds_zero_basis

English

The neighborhood basis of 0 in NNReal is given by sets Iio(a) with a > 0.

Русский

Базис окрестностей нуля в NNReal задаётся множестами Iio(a) при a>0.

LaTeX

$$$(nhds(0)).HasBasis (\\lambda a: 0 < a) (\\lambda a: Iio(a))$$$

Lean4

theorem nhds_zero_basis : (𝓝 (0 : ℝ≥0)).HasBasis (fun a : ℝ≥0 => 0 < a) fun a => Iio a :=
  nhds_bot_basis

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

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

Разделы

Аффилиация

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