Theorems · Theorem · real analysis
BoxIntegral.Prepartition.IsPartition.restrict
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I},
π.IsPartition → J ≤ I → (π.restrict J).IsPartition- Cited by
- 2 results in Mathlib
- Foundations
- Depth 133 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- BoxIntegral.Boxstatement and proof · cited by 464
- BoxIntegral.Prepartitionstatement and proof · cited by 199
- BoxIntegral.Box.toSetproof · cited by 121
- BoxIntegral.Prepartition.IsPartitionstatement and proof · cited by 30
- BoxIntegral.Prepartition.restrictstatement · cited by 16
- BoxIntegral.Prepartition.IsPartition.iUnion_eqproof · cited by 9
- BoxIntegral.Prepartition.isPartition_iff_iUnion_eqproof · cited by 6
- BoxIntegral.Prepartition.iUnion_restrictproof · cited by 3
Cited by2
Results whose statement or proof uses this declaration.
- BoxIntegral.Prepartition.restrict_splitproof · cited by 1
- BoxIntegral.integralSum_inf_partitionproof · cited by 1