closure_eq_self_union_frontier

Mathlib.Topology.Closure

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

English

For any set s, we have closure(s) = s ∪ frontier(s).

Русский

Для любого множества s выполняется closure(s) = s ∪ frontier(s).

LaTeX

$$$\\overline{s} = s \\cup \\operatorname{frontier}(s)$$$

Lean4

theorem closure_eq_self_union_frontier (s : Set X) : closure s = s ∪ frontier s :=
  (union_diff_cancel' interior_subset subset_closure).symm

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

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

Разделы

Аффилиация

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