# Commit 2023-10-16 15:09 b1abe23a

View on Github →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.