English
Let I be a box in the product space, and let i be an index and x a real number. The partition of I given by the boxes I ∩ {y | y_i ≤ x} and I ∩ {y | x < y_i} forms a partition of I; if one of these boxes is empty, the partition reduces to the trivial partition ⊤.
Русский
Пусть I — коробка в пространстве, пусть i — индекс, а x — действительное число. Разбиение I на коробки I ∩ {y | y_i ≤ x} и I ∩ {y | x < y_i} образует разбиение I; если одна из частей пустая, разбиение равно тривиальному разбиению ⊤.
LaTeX
$$$\\mathrm{IsPartition}\\big(\\mathrm{split}\\ I\\ i\\ x\\big)$$$
Lean4
/-- The partition of `I : Box ι` into the boxes `I ∩ {y | y ≤ x i}` and `I ∩ {y | x i < y}`.
One of these boxes can be empty, then this partition is just the single-box partition `⊤`. -/
def split (I : Box ι) (i : ι) (x : ℝ) : Prepartition I :=
ofWithBot {I.splitLower i x, I.splitUpper i x}
(by
simp only [Finset.mem_insert, Finset.mem_singleton]
rintro J (rfl | rfl)
exacts [Box.splitLower_le, Box.splitUpper_le])
(by
simp only [Finset.coe_insert, Finset.coe_singleton, true_and, Set.mem_singleton_iff,
pairwise_insert_of_symmetric symmetric_disjoint, pairwise_singleton]
rintro J rfl -
exact I.disjoint_splitLower_splitUpper i x)
