closure_empty_iff

Mathlib.Topology.Closure

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

English

closure s = ∅ if and only if s = ∅.

Русский

closure s = ∅, если и только если s = ∅.

LaTeX

$$closure s = ∅ \iff s = ∅$$

Lean4

@[simp]
theorem closure_empty_iff (s : Set X) : closure s = ∅ ↔ s = ∅ :=
  ⟨subset_eq_empty subset_closure, fun h => h.symm ▸ closure_empty⟩

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

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

Разделы

Аффилиация

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