nhdsSet_basis_nhdsKer

Mathlib.Topology.AlexandrovDiscrete

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

← MathLib Explorer

English

The neighborhood system nhdsSet s has a basis given by nhdsKer s.

Русский

Система окрестностей nhdsSet s имеет базис, задаваемый nhdsKer s.

LaTeX

$$(nhdsSet s).HasBasis (fun _ : Unit => True) (fun _ => nhdsKer s)$$

Lean4

theorem nhdsSet_basis_nhdsKer (s : Set α) : (𝓝ˢ s).HasBasis (fun _ : Unit => True) (fun _ => nhdsKer s) :=
  principal_nhdsKer s ▸ hasBasis_principal (nhdsKer s)

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

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

Разделы

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

Аффилиация

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