boundary_disjointUnion — Mathlib

English

The boundary of a disjoint union equals the union of the images of the boundaries of each part.

Русский

Граница несмещенного объединения равна объединению образов границ частей.

LaTeX

$$ModelWithCorners.boundary (I := I) (M ⊕ M') = Sum.inl '' (ModelWithCorners.boundary (I := I) M) ∪ Sum.inr '' (ModelWithCorners.boundary (I := I) M')$$

Lean4

theorem boundary_disjointUnion :
    ModelWithCorners.boundary (I := I) (M ⊕ M') =
      Sum.inl '' (ModelWithCorners.boundary (I := I) M) ∪ Sum.inr '' (ModelWithCorners.boundary (I := I) M') :=
  by simp only [← ModelWithCorners.compl_interior, interior_disjointUnion, inl_compl_union_inr_compl]

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