Theorems · Theorem · real analysis

BoxIntegral.Box.splitUpper_def

∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : DecidableEq ι] {i : ι} {x : ℝ}
  (h : x ∈ Set.Ioo (I.lower i) (I.upper i)) (h' : optParam (∀ (j : ι), Function.update I.lower i x j < I.upper j) ⋯),
  I.splitUpper i x = ↑{ lower := Function.update I.lower i x, upper := I.upper, lower_lt_upper := h' }

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Split

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEq