splitCenter — Mathlib

English

Split a box I in Euclidean space into 2^n boxes by hyperplanes through its center; this is a center split prepartition.

Русский

Разбиваем прямоугольник I в n-мерной евклидовой области гиперплоскостями через его центр на 2^n частей.

LaTeX

$$$ \\text{splitCenter}(I) \\text{ is a prepartition with exactly } 2^{n} \\text{ boxes} $$$

Lean4

/-- Split a box in `ℝⁿ` into `2 ^ n` boxes by hyperplanes passing through its center. -/
def splitCenter (I : Box ι) : Prepartition I
    where
  boxes := Finset.univ.map (Box.splitCenterBoxEmb I)
  le_of_mem' := by simp [I.splitCenterBox_le]
  pairwiseDisjoint := by
    rw [Finset.coe_map, Finset.coe_univ, image_univ]
    rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩ Hne
    exact I.disjoint_splitCenterBox (mt (congr_arg _) Hne)

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