English
If hC is a SetSemiring and s ⊆ t with hs ∈ C, ht ∈ C, then m t = m s + ∑_{i ∈ hC.disjointOfDiff ht hs} m i.
Русский
Если hC — множество полуполей и s ⊆ t, причём s,t ∈ C, то m(t) = m(s) + ∑_{i ∈ hC.disjointOfDiff ht hs} m(i).
LaTeX
$$$$ m t = m s + \\sum_{i \\in hC.disjointOfDiff ht hs} m i. $$$$
Lean4
/-- For an `m : addContent C` on a `SetSemiring C` and `s t : Set α` with `s ⊆ t`, we can write
`m t = m s + ∑ i in hC.disjointOfDiff ht hs, m i`. -/
theorem eq_add_disjointOfDiff_of_subset (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) (hst : s ⊆ t) :
m t = m s + ∑ i ∈ hC.disjointOfDiff ht hs, m i := by
classical
conv_lhs => rw [← hC.sUnion_insert_disjointOfDiff ht hs hst]
rw [← coe_insert, addContent_sUnion]
· rw [sum_insert]
exact hC.notMem_disjointOfDiff ht hs
· rw [coe_insert]
exact Set.insert_subset hs (hC.subset_disjointOfDiff ht hs)
· rw [coe_insert]
exact hC.pairwiseDisjoint_insert_disjointOfDiff ht hs
· rw [coe_insert]
rwa [hC.sUnion_insert_disjointOfDiff ht hs hst]
