Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-04 08:09 08770779

View on Github →

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.

Estimated changes