nhdsKer_eq_iff_isOpen

Mathlib.Topology.AlexandrovDiscrete

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

English

nhdsKer s = s if and only if s is open.

Русский

nhdsKer s = s тогда и только тогда, когда s открыто.

LaTeX

$$nhdsKer s = s \\iff IsOpen s$$

Lean4

@[simp]
theorem nhdsKer_eq_iff_isOpen : nhdsKer s = s ↔ IsOpen s :=
  ⟨fun h ↦ h ▸ isOpen_nhdsKer, IsOpen.nhdsKer_eq⟩

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

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

Разделы

Аффилиация

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