Commit 2021-07-09 19:00 a444e81f
View on Github →feat(measure_theory/borel_space): a preconnected set is measurable (#8044) In a conditionally complete linear order equipped with the order topology and the corresponding borel σ-algebra, any preconnected set is measurable.