interior_union_boundary_eq_univ — Mathlib

English

The interior and boundary together cover the entire manifold: I.interior M ∪ I.boundary M = univ.

Русский

Внутреннее пространство и граница вместе охватывают все множество: I.interior M ∪ I.boundary M = univ.

LaTeX

$$$$ (I.interior M) \cup (I.boundary M) = (univ : Set M) $$$$

Lean4

/-- A manifold decomposes into interior and boundary. -/
theorem interior_union_boundary_eq_univ : (I.interior M) ∪ (I.boundary M) = (univ : Set M) :=
  eq_univ_of_forall fun x => (mem_union _ _ _).mpr (I.isInteriorPoint_or_isBoundaryPoint x)

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