nhds_basis_nhdsKer_singleton

Mathlib.Topology.AlexandrovDiscrete

URI: https://scilib.ai/kg/mathlib#nhds_basis_nhdsKer_singleton

← MathLib Explorer

English

The neighborhood basis at a equals nhdsKer of the singleton {a}.

Русский

Базис окрестностей в a равен nhdsKer от множества {a}.

LaTeX

$$nhds a HasBasis (fun x => True) (fun x => nhdsKer { a })$$

Lean4

theorem nhds_basis_nhdsKer_singleton (a : α) : (𝓝 a).HasBasis (fun _ : Unit => True) (fun _ => nhdsKer { a }) :=
  principal_nhdsKer_singleton a ▸ hasBasis_principal (nhdsKer { a })

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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