Theorems · Definition · real analysis
BoxIntegral.IntegrationParams.bRiemann
BoxIntegral.IntegrationParams → Bool
true if the filter corresponds to a Riemann-style integral,
i.e. in the definition of integrability we require a constant upper estimate r on the size of
boxes of a tagged partition; the value false means that the estimate may depend on the position
of the tag.
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 1 from the axioms · 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.IntegrationParamsstatement and proof · cited by 101
Cited by17
Results whose statement or proof uses this declaration.
- BoxIntegral.IntegrationParams.RCondproof · cited by 16
- BoxIntegral.IntegrationParams.rCond_of_bRiemann_eq_falsestatement and proof · cited by 4
- BoxIntegral.IntegrationParams.hasBasis_toFilterDistortionproof · cited by 3
- BoxIntegral.integrable_of_bounded_and_ae_continuousWithinAtproof · cited by 2
- BoxIntegral.HasIntegral.of_bRiemann_eq_false_of_forall_isLittleOstatement and proof · cited by 2
- BoxIntegral.Integrable.convergenceR_condproof · cited by 2
- MeasureTheory.IntegrableOn.hasBoxIntegralstatement and proof · cited by 2
- MeasureTheory.SimpleFunc.hasBoxIntegralstatement and proof · cited by 2
- BoxIntegral.hasIntegralIndicatorConststatement and proof · cited by 1
- BoxIntegral.IntegrationParams.extstatement and proof · cited by 1
- BoxIntegral.HasIntegral.congr_aestatement and proof · cited by 1
- BoxIntegral.HasIntegral.of_aeEq_zerostatement and proof · cited by 1