boundary_of_boundaryless_left — Mathlib

English

If M has no boundary, then the boundary of the product M × N is M × ∂N.

Русский

Если M лишено границы, то граница произведения M × N равна M × ∂N.

LaTeX

$$$(\partial M = \emptyset) \Rightarrow \partial(M \times N) = M \times \partial N$$$

Lean4

/-- If `M` is boundaryless, `∂(M×N) = M × ∂N`. -/
theorem boundary_of_boundaryless_left [BoundarylessManifold I M] :
    (I.prod J).boundary (M × N) = Set.prod (univ : Set M) (J.boundary N) :=
  by
  rw [boundary_prod, Boundaryless.boundary_eq_empty (I := I)]
  have : Set.prod (∅ : Set M) (univ : Set N) = ∅ := Set.empty_prod
  rw [this, union_empty]

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