nhds_top_basis

Mathlib.Topology.Instances.ENNReal.Lemmas

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

English

The neighborhood basis at ∞ is given by sets Ioi a with a < ∞.

Русский

Базис окрестностей в ∞ задаётся через множества Ioi a с a < ∞.

LaTeX

$$$\\text{HasBasis}(\\mathcal{N}(\\infty), \\lambda a. a < \\infty, \\lambda a. \\mathrm{Ioi}(a))$$$

Lean4

theorem nhds_top_basis : (𝓝 ∞).HasBasis (fun a => a < ∞) fun a => Ioi a :=
  _root_.nhds_top_basis

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

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

Разделы

Аффилиация

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