English
Given a box I and an index i with x ∈ (I.lower i, I.upper i), the hyperplane {y | y_i = x} splits I into two boxes; Box.splitLower I i x is I ∩ {y | y_i ≤ x} (possibly empty).
Русский
Для коробки I и индекса i с x ∈ (I.lower i, I.upper i) гиперплоскость {y | y_i = x} разбивает I на две коробки; Box.splitLower I i x = I ∩ {y | y_i ≤ x} (возможно пусто).
LaTeX
$$$\\text{splitLower}(I,i,x) = I \\cap \\{ y : y_i \\le x \\}$ (возможно пустое) $$
Lean4
/-- Given a box `I` and `x ∈ (I.lower i, I.upper i)`, the hyperplane `{y : ι → ℝ | y i = x}` splits
`I` into two boxes. `BoxIntegral.Box.splitLower I i x` is the box `I ∩ {y | y i ≤ x}`
(if it is nonempty). As usual, we represent a box that may be empty as
`WithBot (BoxIntegral.Box ι)`. -/
def splitLower (I : Box ι) (i : ι) (x : ℝ) : WithBot (Box ι) :=
mk' I.lower (update I.upper i (min x (I.upper i)))
