English
If x is not strictly between the lower and upper bounds of the i-th coordinate of I, then splitting by x yields the trivial partition ⊤.
Русский
Если x не лежит строго между нижней и верхней границами по координате i в I, то разбиение по x дает тривиальное разбиение ⊤.
LaTeX
$$$x \\notin (I.lowe r i, I.upper i) \\implies \\mathrm{split}\\ I\\ i\\ x = \\top$$$
Lean4
/-- If `x ∉ (I.lower i, I.upper i)`, then the hyperplane `{y | y i = x}` does not split `I`. -/
theorem split_of_notMem_Ioo (h : x ∉ Ioo (I.lower i) (I.upper i)) : split I i x = ⊤ :=
by
refine ((isPartitionTop I).eq_of_boxes_subset fun J hJ => ?_).symm
rcases mem_top.1 hJ with rfl; clear hJ
rw [mem_boxes, mem_split_iff]
rw [mem_Ioo, not_and_or, not_lt, not_lt] at h
cases h <;> [right; left]
· rwa [eq_comm, Box.splitUpper_eq_self]
· rwa [eq_comm, Box.splitLower_eq_self]
