mathlib3 documentation


Order-connected sets are null-measurable #

This file proves that order-connected sets in ℝⁿ under the pointwise order are null-measurable. Recall that x ≤ y iff ∀ i, x i ≤ y i, and s is order-connected iff ∀ x y ∈ s, ∀ z, x ≤ z → z ≤ y → z ∈ s.

Main declarations #

Notes #

We prove null-measurability in ℝⁿ with the -metric, but this transfers directly to ℝⁿ with the Euclidean metric because they have the same measurable sets.

Null-measurability can't be strengthened to measurability because any antichain (and in particular any subset of the antidiagonal {(x, y) | x + y = 0}) is order-connected.


Generalize so that it also applies to ℝ × ℝ, for example.