Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-20 22:44 81c8f310

View on Github →

refactor(analysis/calculus/cont_diff): reorder the file (#13468)

  • There are no functional changes in this PR (except the order of implicit arguments in some lemmas)
  • This PR tries to move cont_diff.comp above some other lemmas. In a follow-up PR I will use this to add lemmas like cont_diff.fst which requires cont_diff.comp, but after this PR we can add it near cont_diff_fst.
  • We also add {m n : with_top ℕ} as variables, so that we don't have to repeat this in every lemma

Estimated changes

modified theorem cont_diff.add
modified theorem cont_diff.comp
modified theorem cont_diff.comp_cont_diff_on
modified theorem cont_diff.cont_diff_at
modified theorem cont_diff.cont_diff_on
modified theorem cont_diff.continuous
modified theorem cont_diff.continuous_deriv
modified theorem cont_diff.continuous_fderiv
modified theorem cont_diff.differentiable
modified theorem cont_diff.mul
modified theorem cont_diff.neg
modified theorem cont_diff.of_le
modified theorem cont_diff.pow
modified theorem cont_diff.prod
modified theorem cont_diff.prod_map
modified theorem cont_diff.smul
modified theorem cont_diff.sub
modified theorem cont_diff_add
modified theorem cont_diff_at.add
modified theorem cont_diff_at.comp
modified theorem cont_diff_at.continuous_at
modified theorem cont_diff_at.mul
modified theorem cont_diff_at.neg
modified theorem cont_diff_at.of_le
modified theorem cont_diff_at.pow
modified theorem cont_diff_at.prod
modified theorem cont_diff_at.smul
modified theorem cont_diff_at.sub
modified theorem cont_diff_at_const
modified theorem cont_diff_at_fst
modified theorem cont_diff_at_id
modified theorem cont_diff_at_map_inverse
modified theorem cont_diff_at_ring_inverse
modified theorem cont_diff_at_snd
modified theorem cont_diff_const
modified theorem cont_diff_fst
modified theorem cont_diff_id
modified theorem cont_diff_iff_cont_diff_at
modified theorem cont_diff_mul
modified theorem cont_diff_neg
modified theorem cont_diff_of_subsingleton
modified theorem cont_diff_on.add
modified theorem cont_diff_on.congr
modified theorem cont_diff_on.congr_mono
modified theorem cont_diff_on.continuous_on
modified theorem cont_diff_on.deriv_of_open
modified theorem cont_diff_on.deriv_within
modified theorem cont_diff_on.fderiv_of_open
modified theorem cont_diff_on.fderiv_within
modified theorem cont_diff_on.mono
modified theorem cont_diff_on.mul
modified theorem cont_diff_on.neg
modified theorem cont_diff_on.of_le
modified theorem cont_diff_on.pow
modified theorem cont_diff_on.prod
modified theorem cont_diff_on.smul
modified theorem cont_diff_on.sub
modified theorem cont_diff_on_congr
modified theorem cont_diff_on_const
modified theorem cont_diff_on_fst
modified theorem cont_diff_on_id
modified theorem cont_diff_on_snd
modified theorem cont_diff_on_univ
modified theorem cont_diff_smul
modified theorem cont_diff_snd
modified theorem cont_diff_within_at.add
modified theorem cont_diff_within_at.comp'
modified theorem cont_diff_within_at.congr'
modified theorem cont_diff_within_at.congr
modified theorem cont_diff_within_at.mono
modified theorem cont_diff_within_at.mul
modified theorem cont_diff_within_at.neg
modified theorem cont_diff_within_at.of_le
modified theorem cont_diff_within_at.pow
modified theorem cont_diff_within_at.prod
modified theorem cont_diff_within_at.smul
modified theorem cont_diff_within_at.sub
modified theorem cont_diff_within_at_const
modified theorem cont_diff_within_at_fst
modified theorem cont_diff_within_at_id
modified theorem cont_diff_within_at_inter'
modified theorem cont_diff_within_at_inter
modified theorem cont_diff_within_at_snd
modified theorem cont_diff_within_at_univ
modified theorem cont_diff_zero_fun
modified theorem linear_isometry.cont_diff