Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-23 22:10 75b1a94a

View on Github →

refactor(analysis/special_functions/exp_log): split into 4 files (#9882)

Estimated changes

added theorem complex.continuous_exp
added theorem complex.exp_bound_sq
added theorem continuous.cexp
added theorem continuous.exp
added theorem continuous_at.cexp
added theorem continuous_at.exp
added theorem continuous_on.cexp
added theorem continuous_on.exp
added theorem filter.tendsto.cexp
added theorem filter.tendsto.exp
added theorem real.comap_exp_at_top
added theorem real.continuous_exp
added theorem real.continuous_on_exp
added theorem real.map_exp_at_bot
added theorem real.map_exp_at_top
added theorem real.range_exp
added theorem complex.deriv_exp
added theorem complex.iter_deriv_exp
added theorem deriv_cexp
added theorem deriv_exp
added theorem deriv_within_cexp
added theorem deriv_within_exp
added theorem differentiable.cexp
added theorem differentiable.exp
added theorem differentiable_at.cexp
added theorem differentiable_at.exp
added theorem differentiable_on.cexp
added theorem differentiable_on.exp
added theorem fderiv_exp
added theorem fderiv_within_exp
added theorem has_deriv_at.cexp
added theorem has_deriv_at.cexp_real
added theorem has_deriv_at.exp
added theorem has_fderiv_at.cexp
added theorem has_fderiv_at.exp
added theorem real.deriv_exp
added theorem real.has_deriv_at_exp
added theorem real.iter_deriv_exp
added theorem times_cont_diff.cexp
added theorem times_cont_diff.exp
added theorem times_cont_diff_at.exp
added theorem times_cont_diff_on.exp
deleted theorem complex.continuous_exp
deleted theorem complex.continuous_on_exp
deleted theorem complex.deriv_exp
deleted theorem complex.exp_bound_sq
deleted theorem complex.has_deriv_at_exp
deleted theorem complex.is_open_map_exp
deleted theorem complex.iter_deriv_exp
deleted theorem continuous.cexp
deleted theorem continuous.log
deleted theorem continuous_at.cexp
deleted theorem continuous_at.log
deleted theorem continuous_on.cexp
deleted theorem continuous_on.log
deleted theorem continuous_within_at.cexp
deleted theorem continuous_within_at.log
deleted theorem deriv.log
deleted theorem deriv_cexp
deleted theorem deriv_exp
deleted theorem deriv_within.log
deleted theorem deriv_within_cexp
deleted theorem deriv_within_exp
deleted theorem differentiable.cexp
deleted theorem differentiable.exp
deleted theorem differentiable.log
deleted theorem differentiable_at.cexp
deleted theorem differentiable_at.exp
deleted theorem differentiable_at.log
deleted theorem differentiable_on.cexp
deleted theorem differentiable_on.exp
deleted theorem differentiable_on.log
deleted theorem fderiv.log
deleted theorem fderiv_exp
deleted theorem fderiv_within.log
deleted theorem fderiv_within_exp
deleted theorem filter.tendsto.cexp
deleted theorem filter.tendsto.log
deleted theorem has_deriv_at.cexp
deleted theorem has_deriv_at.cexp_real
deleted theorem has_deriv_at.exp
deleted theorem has_deriv_at.log
deleted theorem has_deriv_within_at.cexp
deleted theorem has_deriv_within_at.exp
deleted theorem has_deriv_within_at.log
deleted theorem has_fderiv_at.cexp
deleted theorem has_fderiv_at.exp
deleted theorem has_fderiv_at.log
deleted theorem has_fderiv_within_at.cexp
deleted theorem has_fderiv_within_at.exp
deleted theorem has_fderiv_within_at.log
deleted theorem has_strict_deriv_at.cexp
deleted theorem has_strict_deriv_at.exp
deleted theorem has_strict_deriv_at.log
deleted theorem has_strict_fderiv_at.cexp
deleted theorem has_strict_fderiv_at.exp
deleted theorem has_strict_fderiv_at.log
deleted theorem real.comap_exp_at_top
deleted theorem real.continuous_at_log
deleted theorem real.continuous_exp
deleted theorem real.continuous_log'
deleted theorem real.continuous_log
deleted theorem real.continuous_on_exp
deleted theorem real.continuous_on_log
deleted theorem real.deriv_exp
deleted theorem real.deriv_log'
deleted theorem real.deriv_log
deleted theorem real.differentiable_exp
deleted theorem real.exp_log
deleted theorem real.exp_log_eq_abs
deleted theorem real.exp_log_of_neg
deleted def real.exp_order_iso
deleted theorem real.has_deriv_at_exp
deleted theorem real.has_deriv_at_log
deleted theorem real.iter_deriv_exp
deleted theorem real.log_abs
deleted theorem real.log_div
deleted theorem real.log_eq_zero
deleted theorem real.log_exp
deleted theorem real.log_inj_on_pos
deleted theorem real.log_inv
deleted theorem real.log_le_log
deleted theorem real.log_lt_log
deleted theorem real.log_lt_log_iff
deleted theorem real.log_mul
deleted theorem real.log_neg
deleted theorem real.log_neg_eq_log
deleted theorem real.log_neg_iff
deleted theorem real.log_nonneg
deleted theorem real.log_nonneg_iff
deleted theorem real.log_nonpos
deleted theorem real.log_nonpos_iff'
deleted theorem real.log_nonpos_iff
deleted theorem real.log_of_ne_zero
deleted theorem real.log_of_pos
deleted theorem real.log_one
deleted theorem real.log_pos
deleted theorem real.log_pos_iff
deleted theorem real.log_surjective
deleted theorem real.log_zero
deleted theorem real.map_exp_at_bot
deleted theorem real.map_exp_at_top
deleted theorem real.range_exp
deleted theorem real.range_log
deleted theorem real.strict_anti_on_log
deleted theorem real.strict_mono_on_log
deleted theorem real.surj_on_log'
deleted theorem real.surj_on_log
deleted theorem real.tendsto_exp_at_bot
deleted theorem real.tendsto_exp_at_top
deleted theorem real.tendsto_log_at_top
deleted theorem real.times_cont_diff_exp
deleted theorem times_cont_diff.cexp
deleted theorem times_cont_diff.exp
deleted theorem times_cont_diff.log
deleted theorem times_cont_diff_at.cexp
deleted theorem times_cont_diff_at.exp
deleted theorem times_cont_diff_at.log
deleted theorem times_cont_diff_on.cexp
deleted theorem times_cont_diff_on.exp
deleted theorem times_cont_diff_on.log
added theorem continuous.log
added theorem continuous_at.log
added theorem continuous_on.log
added theorem filter.tendsto.log
added theorem real.continuous_at_log
added theorem real.continuous_log'
added theorem real.continuous_log
added theorem real.continuous_on_log
added theorem real.exp_log
added theorem real.exp_log_eq_abs
added theorem real.exp_log_of_neg
added theorem real.log_abs
added theorem real.log_div
added theorem real.log_eq_zero
added theorem real.log_exp
added theorem real.log_inj_on_pos
added theorem real.log_inv
added theorem real.log_le_log
added theorem real.log_lt_log
added theorem real.log_lt_log_iff
added theorem real.log_mul
added theorem real.log_neg
added theorem real.log_neg_eq_log
added theorem real.log_neg_iff
added theorem real.log_nonneg
added theorem real.log_nonneg_iff
added theorem real.log_nonpos
added theorem real.log_nonpos_iff'
added theorem real.log_nonpos_iff
added theorem real.log_of_ne_zero
added theorem real.log_of_pos
added theorem real.log_one
added theorem real.log_pos
added theorem real.log_pos_iff
added theorem real.log_surjective
added theorem real.log_zero
added theorem real.range_log
added theorem real.surj_on_log'
added theorem real.surj_on_log
added theorem deriv.log
added theorem deriv_within.log
added theorem differentiable.log
added theorem differentiable_at.log
added theorem differentiable_on.log
added theorem fderiv.log
added theorem fderiv_within.log
added theorem has_deriv_at.log
added theorem has_fderiv_at.log
added theorem real.deriv_log'
added theorem real.deriv_log
added theorem real.has_deriv_at_log
added theorem times_cont_diff.log
added theorem times_cont_diff_at.log
added theorem times_cont_diff_on.log
modified theorem real.exp_one_near_10
modified theorem real.exp_one_near_20
modified theorem real.log_two_near_10