Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes