Theorem measurable_lt

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 measurable_ltView on Github →
2026-01-26 08:43
Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
feat(MeasureTheory/Probability): Generalize some theorems by replacing OrderClosedTopology with ClosedIciTopology (#34432) …
Modified measurable_ltView on Github →
2025-12-05 16:31
Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
chore(Tactic/Measurability): `fun_prop` lemmas for solving `MeasurableSet {x | ...}` goals (#31592) …
Added measurable_ltView on Github →