mathlib3
317483a6 - feat(analysis/calculus/parametric_integral): generalize, rename (#10397)

Commit
4 years ago
feat(analysis/calculus/parametric_integral): generalize, rename (#10397) * add `integral` to lemma names; * a bit more general `has_fderiv_at_integral_of_dominated_loc_of_lip'`: only require an estimate on `∥F x a - F x₀ a∥` instead of `∥F x a - F y a∥`; * generalize the `deriv` lemmas to `F : 𝕜 → α → E`, `[is_R_or_C 𝕜]`.
Author
Parents
Loading