English
A corollary of existence of approximating sets: given a finite bound, there is a larger P-set t containing s with controlled μ.
Русский
Следствие из существования аппроксимаций: существует множество t с P t и s ⊆ t, контролирующее μ.
LaTeX
$$Corollary of exists_set in inducedOuterMeasure$$
Lean4
/-- To test whether `s` is Carathéodory-measurable we only need to check the sets `t` for which
`P t` holds. See `ofFunction_caratheodory` for another way to show the Carathéodory-measurability
of `s`.
-/
theorem inducedOuterMeasure_caratheodory (s : Set α) :
MeasurableSet[(inducedOuterMeasure m P0 m0).caratheodory] s ↔
∀ t : Set α,
P t →
inducedOuterMeasure m P0 m0 (t ∩ s) + inducedOuterMeasure m P0 m0 (t \ s) ≤ inducedOuterMeasure m P0 m0 t :=
by
rw [isCaratheodory_iff_le]
constructor
· intro h t _ht
exact h t
· intro h u
conv_rhs => rw [inducedOuterMeasure_eq_iInf _ msU m_mono]
refine le_iInf ?_
intro t
refine le_iInf ?_
intro ht
refine le_iInf ?_
intro h2t
refine le_trans ?_ ((h t ht).trans_eq <| inducedOuterMeasure_eq' _ msU m_mono ht)
gcongr
