English
If m is σ-subadditive on a SetSemiring C, then for any f: Nat → Set α with each f(i) ∈ C and the union ∪ f(i) ∈ C, and pairwise disjoint on f, m(⋃ i f(i)) equals the sum of m(f(i)) over i.
Русский
Если m является σ-субаддитивной на SetSemiring C, то для последовательности множеств f(i) ∈ C с попарно непересекающимися f(i) и ∪ f(i) ∈ C выполняется равенство m(⋃ i f(i)) = ∑ m(f(i)).
LaTeX
$$$$ m(\\bigcup_{i} f(i)) = \\sum_{i} m(f(i)). $$$$
Lean4
/-- An `addContent C` on a `SetSemiring C` is sub-additive. -/
theorem addContent_sUnion_le_sum {m : AddContent C} (hC : IsSetSemiring C) (J : Finset (Set α)) (h_ss : ↑J ⊆ C)
(h_mem : ⋃₀ ↑J ∈ C) : m (⋃₀ ↑J) ≤ ∑ u ∈ J, m u := by
classical
have h1 : (disjiUnion J (hC.disjointOfUnion h_ss) (hC.pairwiseDisjoint_disjointOfUnion h_ss) : Set (Set α)) ⊆ C :=
by
simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe, iUnion_subset_iff]
exact fun _ x ↦ hC.disjointOfUnion_subset h_ss x
have h2 :
PairwiseDisjoint (disjiUnion J (hC.disjointOfUnion h_ss) ((hC.pairwiseDisjoint_disjointOfUnion h_ss)) : Set (Set α))
id :=
by
simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe]
exact hC.pairwiseDisjoint_biUnion_disjointOfUnion h_ss
have h3 :
⋃₀ J = ⋃₀ ((disjiUnion J (hC.disjointOfUnion h_ss) (hC.pairwiseDisjoint_disjointOfUnion h_ss)) : Set (Set α)) :=
by
simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe]
exact (Exists.choose_spec (hC.disjointOfUnion_props h_ss)).2.2.2.2.2
rw [h3, addContent_sUnion h1 h2, sum_disjiUnion]
· apply sum_le_sum
intro x hx
refine
sum_addContent_le_of_subset hC (hC.disjointOfUnion_subset h_ss hx)
(hC.pairwiseDisjoint_disjointOfUnion_of_mem h_ss hx) (h_ss hx)
(fun _ s ↦ hC.subset_of_mem_disjointOfUnion h_ss hx s)
· simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe] at *
exact h3.symm ▸ h_mem
