Commit 2023-05-21 17:05 e7aad4d8

View on Github →

feat: port MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap (#4163)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Constructions/BorelSpace/ContinuousLinearMap.lean

added theorem AEMeasurable.apply_continuousLinearMap

added theorem ContinuousLinearMap.measurable_apply'

added theorem ContinuousLinearMap.measurable_apply

added theorem ContinuousLinearMap.measurable_coe

added theorem ContinuousLinearMap.measurable_comp

added theorem Measurable.apply_continuousLinearMap

added theorem aemeasurable_smul_const

added theorem measurable_smul_const