Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-23 00:45 42388681

View on Github →

chore(analysis): rename times_cont_diff (#12227) This replaces times_cont_diff by cont_diff everywhere, and the same for times_cont_mdiff. There is no change at all in content. See https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/times_cont_diff.20name

Estimated changes

added theorem cont_diff.add
added theorem cont_diff.comp
added theorem cont_diff.cont_diff_at
added theorem cont_diff.cont_diff_on
added theorem cont_diff.continuous
added theorem cont_diff.div
added theorem cont_diff.div_const
added theorem cont_diff.inv
added theorem cont_diff.mul
added theorem cont_diff.neg
added theorem cont_diff.of_le
added theorem cont_diff.pow
added theorem cont_diff.prod
added theorem cont_diff.prod_map
added theorem cont_diff.smul
added theorem cont_diff.sub
added theorem cont_diff.sum
added theorem cont_diff_add
added theorem cont_diff_all_iff_nat
added theorem cont_diff_at.add
added theorem cont_diff_at.comp
added theorem cont_diff_at.div
added theorem cont_diff_at.div_const
added theorem cont_diff_at.inv
added theorem cont_diff_at.mul
added theorem cont_diff_at.neg
added theorem cont_diff_at.of_le
added theorem cont_diff_at.pow
added theorem cont_diff_at.prod
added theorem cont_diff_at.prod_map'
added theorem cont_diff_at.prod_map
added theorem cont_diff_at.smul
added theorem cont_diff_at.sub
added theorem cont_diff_at.sum
added def cont_diff_at
added theorem cont_diff_at_const
added theorem cont_diff_at_fst
added theorem cont_diff_at_id
added theorem cont_diff_at_inv
added theorem cont_diff_at_pi
added theorem cont_diff_at_snd
added theorem cont_diff_at_top
added theorem cont_diff_at_zero
added theorem cont_diff_const
added theorem cont_diff_fst
added theorem cont_diff_id
added theorem cont_diff_mul
added theorem cont_diff_neg
added theorem cont_diff_on.add
added theorem cont_diff_on.comp'
added theorem cont_diff_on.comp
added theorem cont_diff_on.congr
added theorem cont_diff_on.div
added theorem cont_diff_on.div_const
added theorem cont_diff_on.inv
added theorem cont_diff_on.mono
added theorem cont_diff_on.mul
added theorem cont_diff_on.neg
added theorem cont_diff_on.of_le
added theorem cont_diff_on.pow
added theorem cont_diff_on.prod
added theorem cont_diff_on.prod_map
added theorem cont_diff_on.smul
added theorem cont_diff_on.sub
added theorem cont_diff_on.sum
added theorem cont_diff_on_congr
added theorem cont_diff_on_const
added theorem cont_diff_on_fst
added theorem cont_diff_on_id
added theorem cont_diff_on_inv
added theorem cont_diff_on_pi
added theorem cont_diff_on_snd
added theorem cont_diff_on_top
added theorem cont_diff_on_univ
added theorem cont_diff_on_zero
added theorem cont_diff_pi
added theorem cont_diff_prod_assoc
added theorem cont_diff_smul
added theorem cont_diff_snd
added theorem cont_diff_top
added theorem cont_diff_within_at_id
added theorem cont_diff_within_at_pi
added theorem cont_diff_zero
added theorem cont_diff_zero_fun
deleted theorem times_cont_diff.add
deleted theorem times_cont_diff.comp
deleted theorem times_cont_diff.div
deleted theorem times_cont_diff.div_const
deleted theorem times_cont_diff.inv
deleted theorem times_cont_diff.mul
deleted theorem times_cont_diff.neg
deleted theorem times_cont_diff.of_le
deleted theorem times_cont_diff.pow
deleted theorem times_cont_diff.prod
deleted theorem times_cont_diff.prod_map
deleted theorem times_cont_diff.smul
deleted theorem times_cont_diff.sub
deleted theorem times_cont_diff.sum
deleted theorem times_cont_diff_add
deleted theorem times_cont_diff_at.add
deleted theorem times_cont_diff_at.comp
deleted theorem times_cont_diff_at.div
deleted theorem times_cont_diff_at.inv
deleted theorem times_cont_diff_at.mul
deleted theorem times_cont_diff_at.neg
deleted theorem times_cont_diff_at.of_le
deleted theorem times_cont_diff_at.pow
deleted theorem times_cont_diff_at.prod
deleted theorem times_cont_diff_at.smul
deleted theorem times_cont_diff_at.sub
deleted theorem times_cont_diff_at.sum
deleted def times_cont_diff_at
deleted theorem times_cont_diff_at_const
deleted theorem times_cont_diff_at_fst
deleted theorem times_cont_diff_at_id
deleted theorem times_cont_diff_at_inv
deleted theorem times_cont_diff_at_pi
deleted theorem times_cont_diff_at_snd
deleted theorem times_cont_diff_at_top
deleted theorem times_cont_diff_at_zero
deleted theorem times_cont_diff_const
deleted theorem times_cont_diff_fst
deleted theorem times_cont_diff_id
deleted theorem times_cont_diff_mul
deleted theorem times_cont_diff_neg
deleted theorem times_cont_diff_on.add
deleted theorem times_cont_diff_on.comp'
deleted theorem times_cont_diff_on.comp
deleted theorem times_cont_diff_on.congr
deleted theorem times_cont_diff_on.div
deleted theorem times_cont_diff_on.inv
deleted theorem times_cont_diff_on.mono
deleted theorem times_cont_diff_on.mul
deleted theorem times_cont_diff_on.neg
deleted theorem times_cont_diff_on.of_le
deleted theorem times_cont_diff_on.pow
deleted theorem times_cont_diff_on.prod
deleted theorem times_cont_diff_on.smul
deleted theorem times_cont_diff_on.sub
deleted theorem times_cont_diff_on.sum
deleted theorem times_cont_diff_on_congr
deleted theorem times_cont_diff_on_const
deleted theorem times_cont_diff_on_fst
deleted theorem times_cont_diff_on_id
deleted theorem times_cont_diff_on_inv
deleted theorem times_cont_diff_on_pi
deleted theorem times_cont_diff_on_snd
deleted theorem times_cont_diff_on_top
deleted theorem times_cont_diff_on_univ
deleted theorem times_cont_diff_on_zero
deleted theorem times_cont_diff_pi
deleted theorem times_cont_diff_smul
deleted theorem times_cont_diff_snd
deleted theorem times_cont_diff_top
deleted theorem times_cont_diff_zero
deleted theorem times_cont_diff_zero_fun
added theorem cont_diff_bump.R_pos
added theorem cont_diff_bump.le_one
added theorem cont_diff_bump.nonneg
added structure cont_diff_bump
added structure cont_diff_bump_of_inner
deleted structure times_cont_diff_bump
added theorem cont_diff.dist
added theorem cont_diff.inner
added theorem cont_diff.norm
added theorem cont_diff.norm_sq
added theorem cont_diff_at.dist
added theorem cont_diff_at.inner
added theorem cont_diff_at.norm
added theorem cont_diff_at.norm_sq
added theorem cont_diff_at_inner
added theorem cont_diff_at_norm
added theorem cont_diff_inner
added theorem cont_diff_norm_sq
added theorem cont_diff_on.dist
added theorem cont_diff_on.inner
added theorem cont_diff_on.norm
added theorem cont_diff_on.norm_sq
deleted theorem times_cont_diff.dist
deleted theorem times_cont_diff.inner
deleted theorem times_cont_diff.norm
deleted theorem times_cont_diff.norm_sq
deleted theorem times_cont_diff_at.dist
deleted theorem times_cont_diff_at.inner
deleted theorem times_cont_diff_at.norm
deleted theorem times_cont_diff_at_inner
deleted theorem times_cont_diff_at_norm
deleted theorem times_cont_diff_inner
deleted theorem times_cont_diff_norm_sq
deleted theorem times_cont_diff_on.dist
deleted theorem times_cont_diff_on.inner
deleted theorem times_cont_diff_on.norm
added theorem complex.cont_diff_exp
added theorem cont_diff.cexp
added theorem cont_diff.exp
added theorem cont_diff_at.cexp
added theorem cont_diff_at.exp
added theorem cont_diff_on.cexp
added theorem cont_diff_on.exp
added theorem real.cont_diff_exp
deleted theorem real.times_cont_diff_exp
deleted theorem times_cont_diff.cexp
deleted theorem times_cont_diff.exp
deleted theorem times_cont_diff_at.cexp
deleted theorem times_cont_diff_at.exp
deleted theorem times_cont_diff_on.cexp
deleted theorem times_cont_diff_on.exp
added theorem cont_diff.log
added theorem cont_diff_at.log
added theorem cont_diff_on.log
added theorem real.cont_diff_at_log
added theorem real.cont_diff_on_log
deleted theorem times_cont_diff.log
deleted theorem times_cont_diff_at.log
deleted theorem times_cont_diff_on.log
added theorem cont_diff.rpow
added theorem cont_diff_at.rpow
added theorem cont_diff_on.rpow
deleted theorem times_cont_diff.rpow
deleted theorem times_cont_diff_at.rpow
deleted theorem times_cont_diff_on.rpow
added theorem cont_diff.sqrt
added theorem cont_diff_at.sqrt
added theorem cont_diff_on.sqrt
added theorem real.cont_diff_at_sqrt
deleted theorem times_cont_diff.sqrt
deleted theorem times_cont_diff_at.sqrt
deleted theorem times_cont_diff_on.sqrt
added theorem cont_diff.arctan
added theorem cont_diff_at.arctan
added theorem cont_diff_on.arctan
added theorem real.cont_diff_arctan
added theorem real.cont_diff_at_tan
deleted theorem times_cont_diff.arctan
deleted theorem times_cont_diff_at.arctan
deleted theorem times_cont_diff_on.arctan
added theorem complex.cont_diff_cos
added theorem complex.cont_diff_cosh
added theorem complex.cont_diff_sin
added theorem complex.cont_diff_sinh
added theorem cont_diff.ccos
added theorem cont_diff.ccosh
added theorem cont_diff.cos
added theorem cont_diff.cosh
added theorem cont_diff.csin
added theorem cont_diff.csinh
added theorem cont_diff.sin
added theorem cont_diff.sinh
added theorem cont_diff_at.ccos
added theorem cont_diff_at.ccosh
added theorem cont_diff_at.cos
added theorem cont_diff_at.cosh
added theorem cont_diff_at.csin
added theorem cont_diff_at.csinh
added theorem cont_diff_at.sin
added theorem cont_diff_at.sinh
added theorem cont_diff_on.ccos
added theorem cont_diff_on.ccosh
added theorem cont_diff_on.cos
added theorem cont_diff_on.cosh
added theorem cont_diff_on.csin
added theorem cont_diff_on.csinh
added theorem cont_diff_on.sin
added theorem cont_diff_on.sinh
added theorem real.cont_diff_cos
added theorem real.cont_diff_cosh
added theorem real.cont_diff_sin
added theorem real.cont_diff_sinh
deleted theorem real.times_cont_diff_cos
deleted theorem real.times_cont_diff_cosh
deleted theorem real.times_cont_diff_sin
deleted theorem real.times_cont_diff_sinh
deleted theorem times_cont_diff.ccos
deleted theorem times_cont_diff.ccosh
deleted theorem times_cont_diff.cos
deleted theorem times_cont_diff.cosh
deleted theorem times_cont_diff.csin
deleted theorem times_cont_diff.csinh
deleted theorem times_cont_diff.sin
deleted theorem times_cont_diff.sinh
deleted theorem times_cont_diff_at.ccos
deleted theorem times_cont_diff_at.ccosh
deleted theorem times_cont_diff_at.cos
deleted theorem times_cont_diff_at.cosh
deleted theorem times_cont_diff_at.csin
deleted theorem times_cont_diff_at.csinh
deleted theorem times_cont_diff_at.sin
deleted theorem times_cont_diff_at.sinh
deleted theorem times_cont_diff_on.ccos
deleted theorem times_cont_diff_on.ccosh
deleted theorem times_cont_diff_on.cos
deleted theorem times_cont_diff_on.cosh
deleted theorem times_cont_diff_on.csin
deleted theorem times_cont_diff_on.csinh
deleted theorem times_cont_diff_on.sin
deleted theorem times_cont_diff_on.sinh
modified theorem smooth_bump_function.R_pos
modified structure smooth_bump_function
added theorem cont_mdiff.comp
added theorem cont_mdiff.continuous
added theorem cont_mdiff.of_le
added theorem cont_mdiff.of_succ
added theorem cont_mdiff.prod_map
added theorem cont_mdiff.prod_mk
added theorem cont_mdiff.smooth
added def cont_mdiff
added theorem cont_mdiff_at.comp
added theorem cont_mdiff_at.of_le
added theorem cont_mdiff_at.of_succ
added theorem cont_mdiff_at.prod_map
added theorem cont_mdiff_at.prod_mk
added def cont_mdiff_at
added theorem cont_mdiff_at_const
added theorem cont_mdiff_at_fst
added theorem cont_mdiff_at_id
added theorem cont_mdiff_at_one
added theorem cont_mdiff_at_pi_space
added theorem cont_mdiff_at_snd
added theorem cont_mdiff_at_top
added theorem cont_mdiff_const
added theorem cont_mdiff_fst
added theorem cont_mdiff_id
added theorem cont_mdiff_iff
added theorem cont_mdiff_iff_target
added theorem cont_mdiff_of_support
added theorem cont_mdiff_on.comp'
added theorem cont_mdiff_on.comp
added theorem cont_mdiff_on.congr
added theorem cont_mdiff_on.mono
added theorem cont_mdiff_on.of_le
added theorem cont_mdiff_on.of_succ
added theorem cont_mdiff_on.prod_map
added theorem cont_mdiff_on.prod_mk
added def cont_mdiff_on
added theorem cont_mdiff_on_chart
added theorem cont_mdiff_on_congr
added theorem cont_mdiff_on_const
added theorem cont_mdiff_on_fst
added theorem cont_mdiff_on_id
added theorem cont_mdiff_on_iff
added theorem cont_mdiff_on_one
added theorem cont_mdiff_on_pi_space
added theorem cont_mdiff_on_snd
added theorem cont_mdiff_on_top
added theorem cont_mdiff_on_univ
added theorem cont_mdiff_one
added theorem cont_mdiff_pi_space
added theorem cont_mdiff_snd
added theorem cont_mdiff_top
added theorem smooth.cont_mdiff
deleted theorem smooth.times_cont_mdiff
modified def smooth
modified def smooth_at
modified theorem smooth_at_id
modified theorem smooth_const
modified theorem smooth_id
modified def smooth_on
modified theorem smooth_on_id
modified theorem smooth_within_at_id
deleted theorem times_cont_mdiff.comp
deleted theorem times_cont_mdiff.of_le
deleted theorem times_cont_mdiff.of_succ
deleted theorem times_cont_mdiff.prod_map
deleted theorem times_cont_mdiff.prod_mk
deleted theorem times_cont_mdiff.smooth
deleted def times_cont_mdiff
deleted theorem times_cont_mdiff_at.comp
deleted theorem times_cont_mdiff_at.of_le
deleted def times_cont_mdiff_at
deleted theorem times_cont_mdiff_at_const
deleted theorem times_cont_mdiff_at_fst
deleted theorem times_cont_mdiff_at_id
deleted theorem times_cont_mdiff_at_one
deleted theorem times_cont_mdiff_at_snd
deleted theorem times_cont_mdiff_at_top
deleted theorem times_cont_mdiff_const
deleted theorem times_cont_mdiff_fst
deleted theorem times_cont_mdiff_id
deleted theorem times_cont_mdiff_iff
deleted theorem times_cont_mdiff_on.comp'
deleted theorem times_cont_mdiff_on.comp
deleted theorem times_cont_mdiff_on.congr
deleted theorem times_cont_mdiff_on.mono
deleted theorem times_cont_mdiff_on.of_le
deleted def times_cont_mdiff_on
deleted theorem times_cont_mdiff_on_chart
deleted theorem times_cont_mdiff_on_congr
deleted theorem times_cont_mdiff_on_const
deleted theorem times_cont_mdiff_on_fst
deleted theorem times_cont_mdiff_on_id
deleted theorem times_cont_mdiff_on_iff
deleted theorem times_cont_mdiff_on_one
deleted theorem times_cont_mdiff_on_snd
deleted theorem times_cont_mdiff_on_top
deleted theorem times_cont_mdiff_on_univ
deleted theorem times_cont_mdiff_one
deleted theorem times_cont_mdiff_pi_space
deleted theorem times_cont_mdiff_snd
deleted theorem times_cont_mdiff_top
added theorem cont_mdiff_map.coe_inj
added theorem cont_mdiff_map.ext
added structure cont_mdiff_map
modified def smooth_map
deleted theorem times_cont_mdiff_map.ext
deleted structure times_cont_mdiff_map
added theorem cont_mdiff_coe_sphere
added theorem cont_mdiff_neg_sphere
added theorem cont_diff_groupoid_le