English
For a family of measures m, the sInf over toCarathéodory equals the carathéodory-measurable set intersection bound (under measurable sets).
Русский
Для семейства мер m, наименьшее Inf по каратэодорной плоскости совпадает с каратэодорной мерой на множествах, измеримых по условию.
LaTeX
$$$ \\text{(sInf over } toCaratheodory) \\text{ is measurable on } s$$$
Lean4
theorem sInf_caratheodory (s : Set α) (hs : MeasurableSet s) :
MeasurableSet[(sInf (toOuterMeasure '' m)).caratheodory] s :=
by
rw [OuterMeasure.sInf_eq_boundedBy_sInfGen]
refine OuterMeasure.boundedBy_caratheodory fun t => ?_
simp only [OuterMeasure.sInfGen, le_iInf_iff, forall_mem_image, measure_eq_iInf t, coe_toOuterMeasure]
intro μ hμ u htu _hu
have hm : ∀ {s t}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ μ t :=
by
intro s t hst
rw [OuterMeasure.sInfGen_def, iInf_image]
exact iInf₂_le_of_le μ hμ <| measure_mono hst
rw [← measure_inter_add_diff u hs]
exact add_le_add (hm <| inter_subset_inter_left _ htu) (hm <| diff_subset_diff_left htu)
