nhdsKer_singleton_subset_iff_mem_nhds

Mathlib.Topology.AlexandrovDiscrete

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

English

For any a ∈ α, nhdsKer {a} ⊆ t iff t ∈ 𝓝 a.

Русский

Для любого a: nhdsKer {a} ⊆ t тогда и только тогда, когда t ∈ 𝓝 a.

LaTeX

$$nhdsKer { a } ⊆ t \\iff t ∈ 𝓝 a$$

Lean4

theorem nhdsKer_singleton_subset_iff_mem_nhds : nhdsKer { a } ⊆ t ↔ t ∈ 𝓝 a := by simp [nhdsKer_subset_iff_mem_nhdsSet]

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

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

Разделы

Аффилиация

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