Theorems · Definition · real analysis

BoxIntegral.Prepartition.ofWithBot

{ι : Type u_1} →
  {I : BoxIntegral.Box ι} →
    (boxes : Finset (WithBot (BoxIntegral.Box ι))) →
      (∀ J ∈ boxes, J ≤ ↑I) → (↑boxes).Pairwise Disjoint → BoxIntegral.Prepartition I

Create a BoxIntegral.Prepartition from a collection of possibly empty boxes by filtering out the empty one if it exists.

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Basic

Cited by

7 results in Mathlib

Foundations

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