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 measure0.
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 : is_antichain has_le.le s) :