Theorems · Definition · real analysis

BoxIntegral.Prepartition.biUnion

{ι : Type u_1} →
  {I : BoxIntegral.Box ι} →
    BoxIntegral.Prepartition I → ((J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) → BoxIntegral.Prepartition I

Given a prepartition π of a box I and a collection of prepartitions πi J of all boxes J ∈ π, returns the prepartition of I into the union of the boxes of all πi J. Though we only use the values of πi on the boxes of π, we require πi to be a globally defined function.

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Basic

Cited by

24 results in Mathlib

Foundations

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