upper_sub_lower_of_mem_splitCenter

English

If J ∈ splitCenter I, then for every i, J.upper i − J.lower i = (I.upper i − I.lower i)/2.

Русский

Если J принадлежит центрированному разбиению I, то по каждой координате i длина по оси i равна половине длины исходного диапазона.

LaTeX

$$$ \\forall i,\\ J.upper i - J.lower i = \\dfrac{I.upper i - I.lower i}{2} $$$

Lean4

theorem upper_sub_lower_of_mem_splitCenter (h : J ∈ splitCenter I) (i : ι) :
    J.upper i - J.lower i = (I.upper i - I.lower i) / 2 :=
  let ⟨s, hs⟩ := mem_splitCenter.1 h
  hs ▸ I.upper_sub_lower_splitCenterBox s i

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