Theorem aemeasurable_restrict_of_antitoneOn

Modification history

2026-10-30 20:28
Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
refactor(MeasureTheory/Constructions/BorelSpace/Order): regroup sections and weaken hypotheses (#45475) …
Modified aemeasurable_restrict_of_antitoneOnView on Github →
2024-05-18 13:04
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
chore(MeasureTheory.Constructions.BorelSpace.Basic): split file (#12470) …
Modified aemeasurable_restrict_of_antitoneOnView on Github →
2023-05-21 12:07
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
feat: port MeasureTheory.Constructions.BorelSpace.Basic (#4018)
Added aemeasurable_restrict_of_antitoneOnView on Github →