Theorems · Definition · real analysis

BoxIntegral.Box.splitUpper

{ι : Type u_1} → BoxIntegral.Box ι → ι → ℝ → WithBot (BoxIntegral.Box ι)

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 ι).

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Split

Cited by

11 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound