boundary_of_boundaryless_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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