Theorem measurableSet_Ici

Modification history

2026-01-26 08:43
Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
feat(MeasureTheory/Probability): Generalize some theorems by replacing OrderClosedTopology with ClosedIciTopology (#34432) …
Modified measurableSet_IciView on Github →
2024-05-18 13:04
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
chore(MeasureTheory.Constructions.BorelSpace.Basic): split file (#12470) …
Modified measurableSet_IciView on Github →
2023-05-21 12:07
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
feat: port MeasureTheory.Constructions.BorelSpace.Basic (#4018)
Added measurableSet_IciView on Github →