compl_frontier_eq_union_interior — Mathlib

English

The complement of the frontier is the union of the interior of s and the interior of the complement of s: (frontier(s))^c = interior(s) ∪ interior(s^c).

Русский

Комплемент границы равен объединению interior(s) и interior(s^c): (frontier(s))^c = interior(s) ∪ interior(s^c).

LaTeX

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

Lean4

theorem compl_frontier_eq_union_interior : (frontier s)ᶜ = interior s ∪ interior sᶜ :=
  by
  rw [frontier_eq_inter_compl_interior]
  simp only [compl_inter, compl_compl]

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