English
The boundary of the product manifold M × N equals ∂M × N ∪ M × ∂N.
Русский
Граница произведения M × N равна ∂M × N ∪ M × ∂N.
LaTeX
$$$$ (I.prod J).boundary (M \times N) = (Set.prod univ (J.boundary N)) \cup ((I.boundary M).prod Set.univ) $$$$
Lean4
/-- The interior of `M × N` is the product of the interiors of `M` and `N`. -/
theorem interior_prod : (I.prod J).interior (M × N) = (I.interior M) ×ˢ (J.interior N) :=
by
ext p
have aux : (interior (range ↑I)) ×ˢ (interior (range J)) = interior (range (I.prod J)) := by
rw [← interior_prod_eq, ← range_prodMap, modelWithCorners_prod_coe]
constructor <;> intro hp
· replace hp : (I.prod J).IsInteriorPoint p := hp
rw [IsInteriorPoint, ← aux] at hp
exact hp
· change (I.prod J).IsInteriorPoint p
rw [IsInteriorPoint, ← aux, mem_prod]
obtain h := Set.mem_prod.mp hp
rw [ModelWithCorners.interior] at h
exact h
