prod — Mathlib

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⟩

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