disjoint_interior_frontier — Mathlib

English

Interior and frontier are disjoint.

Русский

Внутренность и граница множества не перекрываются.

LaTeX

$$$\operatorname{Disjoint}(\operatorname{int}(s), \operatorname{frontier}(s))$$$

Lean4

/-- Interior and frontier are disjoint. -/
theorem disjoint_interior_frontier : Disjoint (interior s) (frontier s) := by
  rw [disjoint_iff_inter_eq_empty, ← closure_diff_interior, diff_eq, ← inter_assoc, inter_comm, ← inter_assoc,
    compl_inter_self, empty_inter]

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