upper_sub_lower_splitCenterBox — Mathlib

English

For any i, the thickness of the center-split box along i is half of the original thickness: (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i)/2.

Русский

Для любой координаты i толщина центр-разделённой коробки вдоль i равна половине исходной толщины: ... = (I.upper i - I.lower i)/2.

LaTeX

$$$$ (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = \frac{I.upper i - I.lower i}{2}. $$$$

Lean4

@[simp]
theorem upper_sub_lower_splitCenterBox (I : Box ι) (s : Set ι) (i : ι) :
    (I.splitCenterBox s).upper i - (I.splitCenterBox s).lower i = (I.upper i - I.lower i) / 2 := by
  by_cases i ∈ s <;> simp [field, splitCenterBox, *] <;> ring

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