Theorems · Theorem · measure theory
intervalIntegral.norm_integral_le_of_norm_le_const
∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b C : ℝ} {f : ℝ → E},
(∀ x ∈ Set.uIoc a b, ‖f x‖ ≤ C) → ‖∫ (x : ℝ) in a..b, f x‖ ≤ C * |b - a|- Cited by
- 3 results in Mathlib
- Foundations
- Depth 260 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Realstatement and proof · cited by 25,697
- NormedAddCommGroupstatement and proof · cited by 15,752
- NormedSpacestatement and proof · cited by 12,499
- Norm.normstatement and proof · cited by 5,413
- absstatement · cited by 1,814
- MeasureTheory.MeasureSpace.volumestatement · cited by 1,323
- intervalIntegralstatement · cited by 546
- Filter.Eventually.of_forallproof · cited by 526
- Set.uIocstatement and proof · cited by 182
- intervalIntegral.norm_integral_le_of_norm_le_const_aeproof · cited by 1
Cited by3
Results whose statement or proof uses this declaration.
- circleIntegral.norm_integral_le_of_norm_le_const'proof · cited by 1
- norm_curveIntegral_segment_leproof · cited by 1
- GaussianFourier.verticalIntegral_norm_leproof · cited by 1