Theorems · Definition · real analysis

BoxIntegral.Prepartition.biUnionTagged

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

Given a partition π of I : BoxIntegral.Box ι and a collection of tagged partitions πi J of all boxes J ∈ π, returns the tagged partition of I into all the boxes of πi J with tags coming from (πi J).tag.

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Tagged

Cited by

13 results in Mathlib

Foundations

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