# 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 #

`Set.OrdConnected.null_frontier`

: The frontier of an order-connected set in`ℝⁿ`

has measure`0`

.

## 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.

## Sketch proof #

- To show an order-connected set is null-measurable, it is enough to show it has null frontier.
- Since an order-connected set is the intersection of its upper and lower closure, it's enough to show that upper and lower sets have null frontier.
- WLOG let's prove it for an upper set
`s`

. - By the Lebesgue density theorem, it is enough to show that any frontier point
`x`

of`s`

is not a Lebesgue point, namely we want the density of`s`

over small balls centered at`x`

to not tend to either`0`

or`1`

. - This is true, since by the upper setness of
`s`

we can intercalate a ball of radius`δ / 4`

in`s`

intersected with the upper quadrant of the ball of radius`δ`

centered at`x`

(recall that the balls are taken in the ∞-norm, so they are cubes), and another ball of radius`δ / 4`

in`sᶜ`

and the lower quadrant of the ball of radius`δ`

centered at`x`

.

## TODO #

Generalize so that it also applies to `ℝ × ℝ`

, for example.

theorem
Set.OrdConnected.nullMeasurableSet
{ι : Type u_1}
[Fintype ι]
{s : Set (ι → ℝ)}
(hs : s.OrdConnected)
:

MeasureTheory.NullMeasurableSet s MeasureTheory.volume