Theorem measurable_eq_mp

Modification history

2026-09-26 09:19
Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean
chore: use `congr()` much more widely (#43408) …
Modified measurable_eq_mpView on Github →
2025-04-03 10:57
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
chore: split `MeasureTheory.MeasurableSpace.Basic` (#23523) …
Modified measurable_eq_mpView on Github →
2025-03-05 21:20
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
chore(MeasureTheory): rename pi family from π to X (#22604) …
Modified measurable_eq_mpView on Github →
2023-10-16 14:39
Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
feat: lemmas for MeasurableSpace.Basic (#7682) …
Added measurable_eq_mpView on Github →