Commit 2021-02-07 13:33 c25dad98

refactor(analysis/calculus/mean_value): use is_R_or_C in more lemmas (#6022)

• use is_R_or_C in convex.norm_image_sub_le* lemmas;
• replace strict_fderiv_of_cont_diff with has_strict_fderiv_at_of_has_fderiv_at_of_continuous_at and has_strict_deriv_at_of_has_deriv_at_of_continuous_at, slightly change assumptions;
• add has_ftaylor_series_up_to_on.has_fderiv_at, has_ftaylor_series_up_to_on.eventually_has_fderiv_at, has_ftaylor_series_up_to_on.differentiable_at;
• add times_cont_diff_at.has_strict_deriv_at and times_cont_diff_at.has_strict_deriv_at';
• prove that complex.exp is strictly differentiable and is an open map;
• add simp lemma interior_mem_nhds.