Theorems · Definition · real analysis
BoxIntegral.IntegrationParams.bHenstock
BoxIntegral.IntegrationParams → Bool
true if we require that each tag belongs to its own closed
box; the value false means that we only require that tags belong to the ambient box.
- Cited by
- 12 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 by15
Results whose statement or proof uses this declaration.
- BoxIntegral.IntegrationParams.MemBaseSet.isHenstockstatement · cited by 6
- BoxIntegral.IntegrationParams.exists_memBaseSet_le_iUnion_eqproof · cited by 2
- BoxIntegral.HasIntegral.of_bRiemann_eq_false_of_forall_isLittleOstatement and proof · cited by 2
- BoxIntegral.IntegrationParams.MemBaseSet.mono'proof · cited by 2
- tendsto_tsum_div_pow_atTop_integralproof · cited by 1
- BoxIntegral.IntegrationParams.biUnionTagged_memBaseSetproof · cited by 1
- BoxIntegral.IntegrationParams.extstatement and proof · cited by 1
- BoxIntegral.IntegrationParams.MemBaseSet.filterproof · cited by 1
- BoxIntegral.HasIntegral.of_le_Henstock_of_forall_isLittleOproof · cited by 1
- BoxIntegral.IntegrationParams.MemBaseSet.unionComplToSubordinateproof · cited by 1
- BoxIntegral.IntegrationParams.equivProdproof · cited by 0
- BoxIntegral.IntegrationParams.ext_iffstatement and proof · cited by 0