# mathlib3documentation

measure_theory.order.upper_lower

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

## TODO #

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

theorem is_upper_set.null_frontier {ι : Type u_1} [fintype ι] {s : set )} (hs : is_upper_set s) :
theorem is_lower_set.null_frontier {ι : Type u_1} [fintype ι] {s : set )} (hs : is_lower_set s) :
theorem set.ord_connected.null_frontier {ι : Type u_1} [fintype ι] {s : set )} (hs : s.ord_connected) :
@[protected]
theorem set.ord_connected.null_measurable_set {ι : Type u_1} [fintype ι] {s : set )} (hs : s.ord_connected) :
theorem is_antichain.volume_eq_zero {ι : Type u_1} [fintype ι] {s : set )} [nonempty ι] (hs : s) :