coborder_eq_union_frontier_compl — Mathlib

English

The coborder of a set can be decomposed as coborder(s) = s ∪ (frontier(s))^c.

Русский

Граница coborder множества распадается как coborder(s) = s ∪ (frontier(s))^c.

LaTeX

$$$\operatorname{coborder}(s) = s \cup (\operatorname{frontier}(s))^{c}$$$

Lean4

theorem coborder_eq_union_frontier_compl : coborder s = s ∪ (frontier s)ᶜ := by
  rw [coborder, compl_eq_comm, compl_union, compl_compl, ← diff_eq_compl_inter, ← union_diff_right, union_comm, ←
    closure_eq_self_union_frontier]

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