Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-27 07:21 57cc3843

View on Github →

chore(integration): missing lemmas (#7364) These are still preliminaries for derivation of parametric integrals. From the sphere eversion project

Estimated changes

Modified src/analysis/calculus/fderiv_measurable.lean

deleted theorem continuous_linear_map.measurable_apply'

deleted theorem continuous_linear_map.measurable_apply

deleted theorem continuous_linear_map.measurable_coe

Modified src/measure_theory/bochner_integration.lean

added theorem measure_theory.continuous_at_of_dominated

added theorem measure_theory.continuous_of_dominated

Modified src/measure_theory/borel_space.lean

added theorem ae_measurable.apply_continuous_linear_map

added theorem continuous.ae_measurable

added theorem continuous_linear_map.measurable_apply'

added theorem continuous_linear_map.measurable_apply

added theorem continuous_linear_map.measurable_coe

added theorem measurable.apply_continuous_linear_map

Modified src/measure_theory/l1_space.lean

added theorem measure_theory.integrable.apply_continuous_linear_map

added theorem measure_theory.integrable_of_norm_sub_le

Modified src/measure_theory/set_integral.lean

added theorem continuous_linear_map.integral_apply