Theorems · Inductive type · real analysis
BoxIntegral.Prepartition
{ι : Type u_1} → BoxIntegral.Box ι → Type u_1A prepartition of I : BoxIntegral.Box ι is a finite set of pairwise disjoint subboxes of
I.
- Cited by
- 199 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- BoxIntegral.Boxstatement · cited by 464
Cited by244
Results whose statement or proof uses this declaration.
- BoxIntegral.Prepartition.boxesstatement and proof · cited by 77
- BoxIntegral.Prepartition.iUnionstatement and proof · cited by 71
- BoxIntegral.TaggedPrepartition.toPrepartitionstatement · cited by 51
- BoxIntegral.Prepartition.IsPartitionstatement and proof · cited by 30
- BoxIntegral.Prepartition.biUnionstatement and proof · cited by 24
- BoxIntegral.Prepartition.distortionstatement and proof · cited by 23
- MeasureTheory.Measure.toBoxAdditiveproof · cited by 22
- BoxIntegral.IntegrationParams.toFilteriUnionstatement and proof · cited by 16
- BoxIntegral.Prepartition.restrictstatement and proof · cited by 16
- BoxIntegral.Prepartition.le_of_memstatement and proof · cited by 15
- BoxIntegral.Prepartition.filterstatement and proof · cited by 14
- BoxIntegral.Prepartition.splitstatement · cited by 14
Showing the 200 most cited of 244.