English
The boundary of the product manifold equals ∂M × N ∪ M × ∂N, equivalently the boundary of the product equals the union of product with boundaries.
Русский
Граница произведения равна ∂M × N ∪ M × ∂N, то есть объединение произведений с границами.
LaTeX
$$$$ (I.prod J).boundary (M × N) = Set.prod univ (J.boundary N) \cup (I.boundary M).prod Set.univ $$$$
Lean4
/-- The boundary of `M × N` is `∂M × N ∪ (M × ∂N)`. -/
theorem boundary_prod : (I.prod J).boundary (M × N) = Set.prod univ (J.boundary N) ∪ Set.prod (I.boundary M) univ :=
by
let h :=
calc
(I.prod J).boundary (M × N)
_ = ((I.prod J).interior (M × N))ᶜ := compl_interior.symm
_ = ((I.interior M) ×ˢ (J.interior N))ᶜ := by rw [interior_prod]
_ = (I.interior M)ᶜ ×ˢ univ ∪ univ ×ˢ (J.interior N)ᶜ := by rw [compl_prod_eq_union]
rw [h, I.compl_interior, J.compl_interior, union_comm]
rfl
