English
Removing a face along coordinate i splits the product: the product over the face coordinates times the i-th side equals the full product.
Русский
Удаление грани по координате i даёт разложение произведения: произведение по граням по всем координатам равно полному произведению.
LaTeX
$$$\\left(\\prod_{j}((I.face i).upper j - (I.face i).lower j)\\right) \\cdot (I.upper i - I.lower i) = \\prod_{j}(I.upper j - I.lower j)$$$
Lean4
theorem volume_face_mul {n} (i : Fin (n + 1)) (I : Box (Fin (n + 1))) :
(∏ j, ((I.face i).upper j - (I.face i).lower j)) * (I.upper i - I.lower i) = ∏ j, (I.upper j - I.lower j) := by
simp only [face_lower, face_upper, Fin.prod_univ_succAbove _ i, mul_comm]