Theorem measurable_id'

Modification history

2026-09-21 08:35

Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

feat(MeasureTheory): measurability of a function defined by `ite` (#43291) …

Modified measurable_id'View on Github →

2023-02-06 20:02

Mathlib/MeasureTheory/MeasurableSpaceDef.lean

feat: port MeasureTheory.MeasurableSpaceDef (#2108)

Added measurable_id'View on Github →