Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-18 14:41 0ededd5d

View on Github →

chore(analysis/calculus): use is_R_or_C in several lemmas (#10376)

Estimated changes

Modified src/analysis/calculus/mean_value.lean

modified theorem convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at

modified theorem convex.exists_nhds_within_lipschitz_on_with_of_has_fderiv_within_at_of_nnnorm_lt

modified theorem convex.is_const_of_fderiv_within_eq_zero

modified theorem convex.lipschitz_on_with_of_nnnorm_deriv_le

modified theorem convex.lipschitz_on_with_of_nnnorm_deriv_within_le

modified theorem convex.lipschitz_on_with_of_nnnorm_fderiv_le

modified theorem convex.lipschitz_on_with_of_nnnorm_fderiv_within_le

modified theorem convex.lipschitz_on_with_of_nnnorm_has_deriv_within_le

modified theorem convex.lipschitz_on_with_of_nnnorm_has_fderiv_within_le

modified theorem convex.norm_image_sub_le_of_norm_deriv_le

modified theorem convex.norm_image_sub_le_of_norm_deriv_within_le

modified theorem convex.norm_image_sub_le_of_norm_fderiv_le'

modified theorem convex.norm_image_sub_le_of_norm_fderiv_le

modified theorem convex.norm_image_sub_le_of_norm_fderiv_within_le'

modified theorem convex.norm_image_sub_le_of_norm_fderiv_within_le

modified theorem convex.norm_image_sub_le_of_norm_has_deriv_within_le

modified theorem convex.norm_image_sub_le_of_norm_has_fderiv_within_le'

modified theorem convex.norm_image_sub_le_of_norm_has_fderiv_within_le

modified theorem is_const_of_fderiv_eq_zero