nhds_zero_basis_Iic

Mathlib.Topology.Instances.ENNReal.Lemmas

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

English

The HasBasis for nhds 0 with Iic basis on a>0.

Русский

HasBasis для nhds 0 с базисом через Iic и a>0.

LaTeX

$$$ (nhds(0)).HasBasis (\\lambda a: a>0) Iic $$$

Lean4

theorem nhds_zero_basis_Iic : (𝓝 (0 : ℝ≥0∞)).HasBasis (fun a : ℝ≥0∞ => 0 < a) Iic :=
  nhds_bot_basis_Iic

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

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

Разделы

Аффилиация

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