upper_sub_lower — Mathlib

English

For Box unit partition, the difference of upper and lower in any coordinate is 1/n.

Русский

Разность верхней и нижней граней по любой координате равна 1/n.

LaTeX

$$$(\text{box}(n,\nu).\mathrm{upper}_i) - (\text{box}(n,\nu).\mathrm{lower}_i) = \frac{1}{n}$$$

Lean4

theorem upper_sub_lower (ν : ι → ℤ) (i : ι) : (box n ν).upper i - (box n ν).lower i = 1 / n := by
  simp_rw [box, add_div, add_sub_cancel_left]

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