closure_eq_interior_union_frontier

English

For any set s, the closure of s is the union of its interior and its frontier: closure(s) = interior(s) ∪ frontier(s).

Русский

Замыкание множества s равно объединению его interior и frontier: closure(s) = interior(s) ∪ frontier(s).

LaTeX

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

Lean4

theorem closure_eq_interior_union_frontier (s : Set X) : closure s = interior s ∪ frontier s :=
  (union_diff_cancel interior_subset_closure).symm

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