English
The induced outer measure from a sigma-subadditive content m coincides with the extension m.extend on sets from the semiring.
Русский
Индуцированная внешняя мера из содержимого σ-субаддитивного совпадает с продолжением m.extend на множествах из полуребра.
LaTeX
$$$\\operatorname{inducedOuterMeasure}(\\lambda x. m x)\\; hC.empty_mem\\; addContent_empty\\ s = m.extend hC s\\quad (s \\in C).$$$
Lean4
/-- For `m : AddContent C` sigma-sub-additive, finite on `C`, the `inducedOuterMeasure` given by `m`
coincides with `m` on `C`. -/
theorem inducedOuterMeasure_eq (hC : IsSetSemiring C) (m : AddContent C) (m_sigma_subadd : m.IsSigmaSubadditive)
(hs : s ∈ C) : inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty s = m s :=
by
suffices inducedOuterMeasure (fun x _ ↦ m x) hC.empty_mem addContent_empty s = m.extend hC s by
rwa [m.extend_eq hC hs] at this
refine Eq.trans ?_ ((m.extend hC).ofFunction_eq hC ?_ ?_ hs)
· congr
· intro f hf hf_mem
rw [m.extend_eq hC hf_mem]
refine (m_sigma_subadd hf hf_mem).trans_eq ?_
congr with i
rw [m.extend_eq hC (hf i)]
· exact fun _ ↦ m.extend_eq_top _
