English
There exists a thickening r with frontier(r) that has zero measure.
Русский
Существует толщинa r такая, что фронтир имеет меру ноль.
LaTeX
$$$\exists r,\; \mu(\text{frontier}(\text{thickening}(r, s))) = 0$$$
Lean4
theorem exists_null_frontier_thickening (μ : Measure Ω) [SFinite μ] (s : Set Ω) {a b : ℝ} (hab : a < b) :
∃ r ∈ Ioo a b, μ (frontier (Metric.thickening r s)) = 0 :=
by
have mbles : ∀ r : ℝ, MeasurableSet (frontier (Metric.thickening r s)) := fun r ↦ isClosed_frontier.measurableSet
have disjs := Metric.frontier_thickening_disjoint s
have key := Measure.countable_meas_pos_of_disjoint_iUnion (μ := μ) mbles disjs
have aux := measure_diff_null (s := Ioo a b) (Set.Countable.measure_zero key volume)
have len_pos : 0 < ENNReal.ofReal (b - a) := by simp only [hab, ENNReal.ofReal_pos, sub_pos]
rw [← Real.volume_Ioo, ← aux] at len_pos
rcases nonempty_of_measure_ne_zero len_pos.ne.symm with ⟨r, ⟨r_in_Ioo, hr⟩⟩
refine ⟨r, r_in_Ioo, ?_⟩
simpa only [mem_setOf_eq, not_lt, le_zero_iff] using hr
