English
Let C be a semiring of sets. For a sigma-subadditive content m finite on C, and any s ∈ C, the outer measure built from m agrees with m on s.
Русский
Пусть C — полуребро множеств. Для содержимого m, субаддитивного по совокупности и конечного на C, внешняя мера, построенная из m, совпадает с m на любом s ∈ C.
LaTeX
$$$\\text{If } hs: s \\in C,\\quad \\operatorname{OuterMeasure.ofFunction} m\\; addContent\\_empty\\ s = m\\,s.$$$
Lean4
/-- For `m : AddContent C` sigma-sub-additive, finite on `C`, the `OuterMeasure` given by `m`
coincides with `m` on `C`. -/
theorem ofFunction_eq (hC : IsSetSemiring C) (m : AddContent C) (m_sigma_subadd : m.IsSigmaSubadditive)
(m_top : ∀ s ∉ C, m s = ∞) (hs : s ∈ C) : OuterMeasure.ofFunction m addContent_empty s = m s :=
by
refine le_antisymm (OuterMeasure.ofFunction_le s) ?_
rw [OuterMeasure.ofFunction_eq_iInf_mem _ _ m_top]
refine le_iInf fun f ↦ le_iInf fun hf ↦ le_iInf fun hs_subset ↦ ?_
calc
m s = m (s ∩ ⋃ i, f i) := by rw [inter_eq_self_of_subset_left hs_subset]
_ = m (⋃ i, s ∩ f i) := by rw [inter_iUnion]
_ ≤ ∑' i, m (s ∩ f i) := by
refine m_sigma_subadd (fun i ↦ hC.inter_mem _ hs _ (hf i)) ?_
rwa [← inter_iUnion, inter_eq_self_of_subset_left hs_subset]
_ ≤ ∑' i, m (f i) := by
refine ENNReal.summable.tsum_le_tsum (fun i ↦ ?_) ENNReal.summable
exact addContent_mono hC (hC.inter_mem _ hs _ (hf i)) (hf i) Set.inter_subset_right
