Theorem ContinuousLinearMap.measurable_coe

Modification history

2023-05-21 17:05

Mathlib/MeasureTheory/Constructions/BorelSpace/ContinuousLinearMap.lean

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

Added ContinuousLinearMap.measurable_coe View on Github →