English
The product of two boundaryless manifolds is boundaryless.
Русский
Произведение двух многообразий без границы тоже без границы.
LaTeX
$$BoundarylessManifold(I, M) \land BoundarylessManifold(J, N) \Rightarrow BoundarylessManifold(I \cdot J, M \times N)$$
Lean4
/-- The product of two boundaryless manifolds is boundaryless. -/
instance prod [BoundarylessManifold I M] [BoundarylessManifold J N] : BoundarylessManifold (I.prod J) (M × N) :=
by
apply Boundaryless.of_boundary_eq_empty
simp only [boundary_prod, Boundaryless.boundary_eq_empty, union_empty_iff]
-- These are simp lemmas, but `simp` does not apply them on its own:
-- presumably because of the distinction between `Prod` and `ModelProd`
exact ⟨Set.prod_empty, Set.empty_prod⟩