Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 17:29 e49ac91b

View on Github →

feat(analysis/calculus/cont_diff): add more prod lemmas (#13521)

  • Add cont_diff.fst, cont_diff.comp₂, cont_diff_prod_mk_left and many variants.
  • From the sphere eversion project
  • Required for convolutions
  • PR #13423 is similar for continuity

Estimated changes

modified theorem cont_diff.comp_cont_diff_at
added theorem cont_diff.comp₂
added theorem cont_diff.comp₃
modified theorem cont_diff.cont_diff_at
modified theorem cont_diff.cont_diff_on
modified theorem cont_diff.continuous
modified theorem cont_diff.differentiable
added theorem cont_diff.fst'
added theorem cont_diff.fst
modified theorem cont_diff.of_le
added theorem cont_diff.of_succ
added theorem cont_diff.one_of_succ
added theorem cont_diff.snd'
added theorem cont_diff.snd
modified theorem cont_diff_all_iff_nat
added theorem cont_diff_apply
added theorem cont_diff_apply_apply
added theorem cont_diff_at.fst''
added theorem cont_diff_at.fst'
added theorem cont_diff_at.fst
added theorem cont_diff_at.snd''
added theorem cont_diff_at.snd'
added theorem cont_diff_at.snd
modified theorem cont_diff_at_fst
modified theorem cont_diff_at_snd
modified theorem cont_diff_at_zero
modified theorem cont_diff_iff_cont_diff_at
added theorem cont_diff_on.fst
added theorem cont_diff_on.snd
modified theorem cont_diff_on_fst
modified theorem cont_diff_on_snd
modified theorem cont_diff_on_univ
added theorem cont_diff_prod_mk_left
modified theorem cont_diff_top
modified theorem cont_diff_zero