Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-13 11:15 1a233e0e

View on Github →

feat(analysis/calculus): derivative is measurable (#4974)

Estimated changes

Modified src/analysis/calculus/fderiv.lean

added theorem fderiv_mem_iff

Created src/analysis/calculus/fderiv_measurable.lean

added theorem continuous_linear_map.measurable_apply'

added theorem continuous_linear_map.measurable_apply

added theorem continuous_linear_map.measurable_apply₂

added theorem continuous_linear_map.measurable_coe

added def fderiv_measurable_aux.A

added theorem fderiv_measurable_aux.A_mono

added def fderiv_measurable_aux.B

added def fderiv_measurable_aux.D

added theorem fderiv_measurable_aux.D_subset_differentiable_set

added theorem fderiv_measurable_aux.differentiable_set_eq_D

added theorem fderiv_measurable_aux.differentiable_set_subset_D

added theorem fderiv_measurable_aux.is_open_A

added theorem fderiv_measurable_aux.is_open_B

added theorem fderiv_measurable_aux.le_of_mem_A

added theorem fderiv_measurable_aux.mem_A_of_differentiable

added theorem fderiv_measurable_aux.norm_sub_le_of_mem_A

added theorem is_measurable_set_of_differentiable_at

added theorem is_measurable_set_of_differentiable_at_of_is_complete

added theorem measurable_deriv

added theorem measurable_fderiv

added theorem measurable_fderiv_apply_const

Modified src/topology/metric_space/premetric_space.lean