English
Given a SetSemiring C and a family of sets I with properties (I ⊆ C), a subset of C, and pairwise disjointness, the value of m on s can be decomposed as m(s) = ∑_{i∈I} m(i) + ∑_{i ∈ disjointOfDiffUnion} m(i).
Русский
Пусть C задаёт множество полупалей, и I — конечное множество, удовлетворяющее условиям; тогда значение m на s разлагается как m(s) = ∑_{i∈I} m(i) + ∑_{i ∈ disjointOfDiffUnion} m(i).
LaTeX
$$$$ m s = \\sum_{i \\in I} m i + \\sum_{i \\in hC.disjointOfDiffUnion hs hI} m i. $$$$
Lean4
theorem addContent_eq_add_disjointOfDiffUnion_of_subset (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C)
(hI_ss : ∀ t ∈ I, t ⊆ s) (h_dis : PairwiseDisjoint (I : Set (Set α)) id) :
m s = ∑ i ∈ I, m i + ∑ i ∈ hC.disjointOfDiffUnion hs hI, m i := by
classical
conv_lhs => rw [← hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]
rw [addContent_sUnion]
· rw [sum_union]
exact hC.disjoint_disjointOfDiffUnion hs hI
· rw [coe_union]
exact Set.union_subset hI (hC.disjointOfDiffUnion_subset hs hI)
· rw [coe_union]
exact hC.pairwiseDisjoint_union_disjointOfDiffUnion hs hI h_dis
· rwa [hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]
