English
If hs holds for all t, then the Carathéodory measure of the constructed outer measure is measurable on s.
Русский
Если для всех t выполнено неравенство hs, то множество s является карatheодory-измеримым относительно OuterMeasure.ofFunction m h₀.
LaTeX
$$MeasurableSet[(OuterMeasure.ofFunction m h₀).caratheodory] s$$
Lean4
theorem ofFunction_caratheodory {m : Set α → ℝ≥0∞} {s : Set α} {h₀ : m ∅ = 0} (hs : ∀ t, m (t ∩ s) + m (t \ s) ≤ m t) :
MeasurableSet[(OuterMeasure.ofFunction m h₀).caratheodory] s :=
by
apply (isCaratheodory_iff_le _).mpr
refine fun t => le_iInf fun f => le_iInf fun hf => ?_
refine
le_trans
(add_le_add ((iInf_le_of_le fun i => f i ∩ s) <| iInf_le _ ?_) ((iInf_le_of_le fun i => f i \ s) <| iInf_le _ ?_))
?_
· rw [← iUnion_inter]
exact inter_subset_inter_left _ hf
· rw [← iUnion_diff]
exact diff_subset_diff_left hf
· rw [← ENNReal.tsum_add]
exact ENNReal.tsum_le_tsum fun i => hs _
