volume_face_mul — Mathlib

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]

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