Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_linear_map.measurable_coe

Modification history

2023-05-15 04:39
src/measure_theory/constructions/borel_space/basic.lean
chore(measure_theory/{constructions/borel_space,integral/lebesgue}): split (#19015) …
Modified continuous_linear_map.measurable_coeView on Github →
2021-04-27 07:21
src/analysis/calculus/fderiv_measurable.lean
chore(integration): missing lemmas (#7364) …
Modified continuous_linear_map.measurable_coeView on Github →
2020-11-13 11:15
src/analysis/calculus/fderiv_measurable.lean
feat(analysis/calculus): derivative is measurable (#4974)
Added continuous_linear_map.measurable_coeView on Github →