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

Modified src/analysis/normed/order/upper_lower.lean

added theorem bdd_above.bounded_inter

added theorem bdd_below.bounded_inter

added theorem bounded_iff_bdd_below_bdd_above

added theorem closure_lower_closure_comm

added theorem closure_upper_closure_comm

added theorem dist_anti_left

added theorem dist_anti_right

added theorem dist_inf_sup

added theorem dist_le_dist_of_le

added theorem dist_mono_left

added theorem dist_mono_right

added theorem is_antichain.interior_eq_empty

added theorem lower_closure_interior_subset'

added theorem upper_closure_interior_subset'

Modified src/data/real/nnreal.lean

added theorem real.to_nnreal_abs

Created src/measure_theory/order/upper_lower.lean

added theorem is_antichain.volume_eq_zero

added theorem is_lower_set.null_frontier

added theorem is_upper_set.null_frontier

added theorem set.ord_connected.null_frontier

Modified src/order/bounds/basic.lean

added theorem mem_lower_bounds_iff_subset_Ici

added theorem mem_upper_bounds_iff_subset_Iic

Modified src/topology/algebra/order/upper_lower.lean

added theorem bdd_above_closure

added theorem bdd_below_closure

added theorem lower_bounds_closure

added theorem upper_bounds_closure