Commit 2026-09-21 08:35 aaa4a978

View on Github →

feat(MeasureTheory): measurability of a function defined by ite (#43291) Also protect Measurable.ite and Measurable.dite, which caused issue to me downstream. From GibbsMeasure

Estimated changes

deleted theorem Measurable.ite
deleted theorem Measurable.dite
added theorem Measurable.dite_const
added theorem Measurable.ite_const
modified theorem Measurable.le
modified theorem measurable_const
modified theorem measurable_id'
modified theorem measurable_id