Theorem Measurable.fun_dite_const

Modification history

2026-09-21 08:35
Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
feat(MeasureTheory): measurability of a function defined by `ite` (#43291) …
Added Measurable.fun_dite_constView on Github →