Theorems · Definition · real analysis
BoxIntegral.Prepartition.splitMany
{ι : Type u_1} → (I : BoxIntegral.Box ι) → Finset (ι × ℝ) → BoxIntegral.Prepartition ISplit a box along many hyperplanes {y | y i = x}; each hyperplane is given by the pair
(i x).
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 138 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Finsetstatement and proof · cited by 13,712
- BoxIntegral.Boxstatement and proof · cited by 464
- Finset.infproof · cited by 219
- BoxIntegral.Prepartitionstatement · cited by 199
- BoxIntegral.Prepartition.splitproof · cited by 14
Cited by13
Results whose statement or proof uses this declaration.
- BoxIntegral.Prepartition.eventually_splitMany_inf_eq_filterstatement and proof · cited by 3
- BoxIntegral.Prepartition.exists_iUnion_eq_sdiffproof · cited by 3
- BoxIntegral.Prepartition.splitMany_insertstatement and proof · cited by 2
- BoxIntegral.Prepartition.isPartition_splitManystatement and proof · cited by 2
- BoxIntegral.Prepartition.iUnion_splitManystatement · cited by 1
- BoxIntegral.Prepartition.inf_splitManystatement and proof · cited by 1
- BoxIntegral.Prepartition.splitMany_le_splitstatement · cited by 1
- BoxIntegral.Prepartition.eventually_not_disjoint_imp_le_of_mem_splitManystatement and proof · cited by 1
- BoxIntegral.Prepartition.exists_splitMany_inf_eq_filter_of_finitestatement · cited by 1
- BoxIntegral.Prepartition.not_disjoint_imp_le_of_subset_of_mem_splitManystatement and proof · cited by 1
- BoxIntegral.Prepartition.splitMany_emptystatement · cited by 0
- BoxIntegral.BoxAdditiveMap.sum_boxes_congrproof · cited by 0