Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-22 09:42 28eb06f9

View on Github →

feat(analysis/calculus): define diff_on_int_cont (#12688)

Estimated changes

Created src/analysis/calculus/diff_on_int_cont.lean

added theorem diff_on_int_cont.add

added theorem diff_on_int_cont.add_const

added theorem diff_on_int_cont.comp

added theorem diff_on_int_cont.const_add

added theorem diff_on_int_cont.const_smul

added theorem diff_on_int_cont.const_sub

added theorem diff_on_int_cont.differentiable_at'

added theorem diff_on_int_cont.differentiable_on_ball

added theorem diff_on_int_cont.inv

added theorem diff_on_int_cont.mk_ball

added theorem diff_on_int_cont.neg

added theorem diff_on_int_cont.smul

added theorem diff_on_int_cont.smul_const

added theorem diff_on_int_cont.sub

added theorem diff_on_int_cont.sub_const

added structure diff_on_int_cont

added theorem diff_on_int_cont_const

added theorem diff_on_int_cont_open

added theorem diff_on_int_cont_univ

added theorem differentiable.comp_diff_on_int_cont

added theorem differentiable.diff_on_int_cont

added theorem differentiable_on.comp_diff_on_int_cont

added theorem differentiable_on.diff_on_int_cont

Modified src/analysis/complex/abs_max.lean

modified theorem complex.norm_max_aux₂

Modified src/analysis/complex/cauchy_integral.lean

deleted theorem complex.circle_integral_sub_inv_smul_of_continuous_on_of_differentiable_on

deleted theorem complex.circle_integral_sub_inv_smul_of_differentiable_on

deleted theorem complex.has_fpower_series_on_ball_of_continuous_on_of_differentiable_on

added theorem diff_on_int_cont.circle_integral_sub_inv_smul

added theorem diff_on_int_cont.has_fpower_series_on_ball

added theorem differentiable_on.circle_integral_sub_inv_smul

Modified src/analysis/complex/liouville.lean

Modified src/analysis/complex/schwarz.lean