English
If an additive content is σ-subadditive on a set ring, then it is σ-additive. In particular, for a sequence of sets f(n) ∈ C with ⋃ f(n) ∈ C and pairwise disjoint {f(n)}, we have m(⋃_n f(n)) = ∑'_n m(f(n)).
Русский
Если аддитивное содержимое на кольце множеств σ-субаддитивно, то оно σ-аддитивно. Пусть последовательность множеств f(n) ∈ C удовлетворяет условию, тогда m(⋃_n f(n)) = ∑'_n m(f(n)).
LaTeX
$$$m\left(\bigcup_{n} f(n)\right) = \sum\nolinebreak'_{n} m\bigl(f(n)\bigr) \quad \text{(при подходящих условиях на } f(n)\text{)}$$$
Lean4
/-- If an `AddContent` is σ-subadditive on a semi-ring of sets, then it is σ-additive. -/
theorem addContent_iUnion_eq_tsum_of_disjoint_of_addContent_iUnion_le {m : AddContent C}
(hC : IsSetSemiring C)
-- TODO: `m_subadd` is in fact equivalent to `m.IsSigmaSubadditive`.
(m_subadd :
∀ (f : ℕ → Set α) (_ : ∀ i, f i ∈ C) (_ : ⋃ i, f i ∈ C) (_hf_disj : Pairwise (Disjoint on f)),
m (⋃ i, f i) ≤ ∑' i, m (f i))
(f : ℕ → Set α) (hf : ∀ i, f i ∈ C) (hf_Union : (⋃ i, f i) ∈ C) (hf_disj : Pairwise (Disjoint on f)) :
m (⋃ i, f i) = ∑' i, m (f i) :=
by
refine le_antisymm (m_subadd f hf hf_Union hf_disj) ?_
refine ENNReal.summable.tsum_le_of_sum_le fun I ↦ ?_
classical
rw [← Finset.sum_image_of_disjoint addContent_empty (hf_disj.pairwiseDisjoint _)]
refine sum_addContent_le_of_subset hC (I := I.image f) ?_ ?_ hf_Union ?_
· simp only [coe_image, Set.image_subset_iff]
refine (subset_preimage_image f I).trans (preimage_mono ?_)
rintro i ⟨j, _, rfl⟩
exact hf j
· simp only [coe_image]
intro s hs t ht hst
rw [Set.mem_image] at hs ht
obtain ⟨i, _, rfl⟩ := hs
obtain ⟨j, _, rfl⟩ := ht
have hij : i ≠ j := by intro h_eq; rw [h_eq] at hst; exact hst rfl
exact hf_disj hij
· simp only [Finset.mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
exact fun i _ ↦ subset_iUnion _ i
