splitUpper — Mathlib

English

Box.splitUpper I i x is the box I ∩ {y | x < y_i} (possibly empty).

Русский

Box.splitUpper I i x — коробка I ∩ {y | x < y_i} (может быть пустой).

LaTeX

$$$\\text{splitUpper}(I,i,x) = I \\cap \\{ y : y_i > 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.splitUpper I i x` is the box `I ∩ {y | x < y i}`
(if it is nonempty). As usual, we represent a box that may be empty as
`WithBot (BoxIntegral.Box ι)`. -/
def splitUpper (I : Box ι) (i : ι) (x : ℝ) : WithBot (Box ι) :=
  mk' (update I.lower i (max x (I.lower i))) I.upper

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