mem_nhdsSet_self

Mathlib.Topology.NhdsSet

URI: https://scilib.ai/kg/mathlib#IsOpen.mem_nhdsSet_self

← MathLib Explorer

English

An open set s belongs to its own set neighborhoods filter 𝓝ˢ s.

Русский

Открытое множество s принадлежит своему собственному фильтру множеств-окрестностей 𝓝ˢ s.

LaTeX

$$$ IsOpen(s) \rightarrow s \in 𝓝ˢ s $$$

Lean4

/-- An open set belongs to its own set neighborhoods filter. -/
theorem mem_nhdsSet_self (ho : IsOpen s) : s ∈ 𝓝ˢ s :=
  ho.mem_nhdsSet.mpr Subset.rfl

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

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

Разделы

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

Аффилиация

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