compl_interior — Mathlib

English

The boundary is the complement of the interior: boundary M = M \ interior M.

Русский

Граница равна дополнению внутренней части: граница M = M \ interior M.

LaTeX

$$$$ I.boundary M = M \ I.interior M $$$$

Lean4

/-- The boundary is the complement of the interior. -/
theorem compl_interior : (I.interior M)ᶜ = I.boundary M :=
  by
  apply compl_unique ?_ I.interior_union_boundary_eq_univ
  exact disjoint_iff_inter_eq_empty.mp I.disjoint_interior_boundary

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