Theorem ContinuousLinearMap.measurable_comp

Modification history

2025-05-11 06:30
Mathlib/MeasureTheory/Constructions/BorelSpace/ContinuousLinearMap.lean
chore(MeasureTheory): relax lots of typeclass assumptions (#24737) …
Modified ContinuousLinearMap.measurable_compView on Github →
2023-05-21 17:05
Mathlib/MeasureTheory/Constructions/BorelSpace/ContinuousLinearMap.lean
feat: port MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap (#4163)
Added ContinuousLinearMap.measurable_compView on Github →