mathlib

a444e81f - feat(measure_theory/borel_space): a preconnected set is measurable (#8044)

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.