mathlib3

b1abe23a - feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (#16976)

feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (#16976) Prove that the frontier of an order-connected set in `ℝⁿ` (with the `∞`-metric, but it doesn't actually matter) has measure zero. As a corollary, antichains in `ℝⁿ` have measure zero. Co-authored-by: @JasonKYi