mathlib3
08770779 - chore(analysis/calculus/times_cont_diff): a few missing lemmas (#4900)

Commit
5 years ago
chore(analysis/calculus/times_cont_diff): a few missing lemmas (#4900) * add `times_cont_diff_within_at_iff_forall_nat_le` and `times_cont_diff_on_iff_forall_nat_le`; * add `times_cont_diff_on_all_iff_nat` and `times_cont_diff_all_iff_nat`; * rename `times_cont_diff_at.differentiable` to `times_cont_diff_at.differentiable_at`; * add `times_cont_diff.div_const`; * add `times_cont_diff_succ_iff_deriv` * move some `of_le` lemmas up to support minor golfing of proofs.
Author
Parents
Loading