Theorems · Inductive type · real analysis
BoxIntegral.Box
Type u_2 → Type u_2
A nontrivial rectangular box in ι → ℝ with corners lower and upper. Represents the product
of half-open intervals (lower i, upper i].
- Defined in
- Mathlib.Analysis.BoxIntegral.Box.Basic
- Cited by
- 464 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by560
Results whose statement or proof uses this declaration.
- BoxIntegral.Prepartitionstatement · cited by 199
- BoxIntegral.TaggedPrepartitionstatement · cited by 126
- BoxIntegral.Box.toSetstatement and proof · cited by 121
- BoxIntegral.BoxAdditiveMapstatement · cited by 92
- BoxIntegral.Prepartition.boxesstatement and proof · cited by 77
- BoxIntegral.Box.Iccstatement and proof · cited by 76
- BoxIntegral.Prepartition.iUnionstatement and proof · cited by 71
- BoxIntegral.Box.upperstatement and proof · cited by 70
- BoxIntegral.Box.lowerstatement and proof · cited by 65
- BoxIntegral.TaggedPrepartition.iUnionstatement and proof · cited by 51
- BoxIntegral.TaggedPrepartition.toPrepartitionstatement and proof · cited by 51
- BoxIntegral.Integrablestatement and proof · cited by 40
Showing the 200 most cited of 560.