nhdsKer_subset_iff_mem_nhdsSet

Mathlib.Topology.AlexandrovDiscrete

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

English

nhdsKer s ⊆ t iff t ∈ 𝓝ˢ s.

Русский

nhdsKer s ⊆ t тогда и только тогда, когда t ∈ 𝓝ˢ s.

LaTeX

$$nhdsKer s ⊆ t \\iff t ∈ \\mathcal{N}^s(s)$$

Lean4

theorem nhdsKer_subset_iff_mem_nhdsSet : nhdsKer s ⊆ t ↔ t ∈ 𝓝ˢ s :=
  nhdsKer_subset_iff.trans mem_nhdsSet_iff_exists.symm

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

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

Разделы

Аффилиация

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