boundaryless_disjointUnion — Mathlib

English

If M and M' are boundaryless, then their disjoint union is boundaryless.

Русский

Если M и M' без границы, то их несмещённое объединение также без границы.

LaTeX

$$BoundarylessManifold I M ∧ BoundarylessManifold I M' ⇒ BoundarylessManifold I (M ⊕ M')$$

Lean4

/-- If `M` and `M'` are boundaryless, so is their disjoint union `M ⊔ M'`. -/
instance boundaryless_disjointUnion [hM : BoundarylessManifold I M] [hM' : BoundarylessManifold I M'] :
    BoundarylessManifold I (M ⊕ M') :=
  by
  rw [← Boundaryless.iff_boundary_eq_empty] at hM hM' ⊢
  simp [boundary_disjointUnion, hM, hM']

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