nhdsKer_eq_empty

Mathlib.Topology.NhdsKer

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

English

The kernel is empty exactly when the set is empty.

Русский

Ядро множества равно пустому тогда и только тогда, когда само множество пусто.

LaTeX

$$$nhdsKer s = \\emptyset \\iff s = \\emptyset$$$

Lean4

@[simp]
theorem nhdsKer_eq_empty : nhdsKer s = ∅ ↔ s = ∅ :=
  ⟨eq_bot_mono subset_nhdsKer, by rintro rfl; exact nhdsKer_empty⟩

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

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

Разделы

Аффилиация

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