English
Let ι be finite and s ⊂ (ι → ℝ) a lower set. Then the frontier of s has Lebesgue volume zero in ℝ^ι.
Русский
Пусть ι конечно, и s ⊂ (ι → ℝ) — нижнее множество. Тогда frontier s имеет нулевой объём в ℝ^ι.
LaTeX
$$$\operatorname{vol}(\partial s)=0$ for s a LowerSet in $(\mathbb{R}^{\!\iota})$ with ι finite.$$
Lean4
theorem null_frontier (hs : IsLowerSet s) : volume (frontier s) = 0 :=
by
refine
measure_mono_null (fun x hx ↦ ?_)
(Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet _ (isClosed_closure (s := s)).measurableSet)
by_cases h : x ∈ closure s <;>
simp only [mem_compl_iff, mem_setOf, h, not_false_eq_true, indicator_of_notMem, indicator_of_mem, Pi.one_apply]
· refine aux₁ fun _ ↦ hs.compl.exists_subset_ball <| frontier_subset_closure ?_
rwa [frontier_compl]
· exact aux₀ fun _ ↦ hs.exists_subset_ball <| frontier_subset_closure hx
