Theorems · Inductive type · real analysis
intervalIntegral.FTCFilter
outParam ℝ → Filter ℝ → outParam (Filter ℝ) → Prop
An auxiliary typeclass for the Fundamental theorem of calculus, part 1. It is used to formulate
theorems that work simultaneously for left and right one-sided derivatives of ∫ x in u..v, f x.
- Cited by
- 25 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.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by27
Results whose statement or proof uses this declaration.
- intervalIntegral.FTCFilter.finiteAt_innerstatement and proof · cited by 4
- intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_aestatement and proof · cited by 3
- intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_rightstatement and proof · cited by 3
- intervalIntegral.integral_hasDerivWithinAt_rightstatement and proof · cited by 3
- intervalIntegral.FTCFilter.pure_lestatement and proof · cited by 3
- intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_aestatement and proof · cited by 2
- intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_leftstatement and proof · cited by 2
- intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_aestatement and proof · cited by 2
- intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_aestatement and proof · cited by 2
- intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_rightstatement and proof · cited by 2
- intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_leftstatement and proof · cited by 1
- intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_rightstatement and proof · cited by 1