English
If hC is a SetSemiring, I is a Finset of sets contained in C, and t ∈ C with union of I contained in t and each s ∈ I is contained in t, then the sum over I of m(s) is less than or equal to m(t).
Русский
Если hC — множество полуполей, I — конечное множество множеств внутри C, и t ∈ C, причём объединение I ⊆ t и каждый s ∈ I ⊆ t, тогда сумма m(s) по s∈I не превосходит m(t).
LaTeX
$$$$ \\sum_{u \\in I} m u \\le m t. $$$$
Lean4
/-- For an `m : addContent C` on a `SetSemiring C`, if `I` is a `Finset` of pairwise disjoint
sets in `C` and `⋃₀ I ⊆ t` for `t ∈ C`, then `∑ s ∈ I, m s ≤ m t`. -/
theorem sum_addContent_le_of_subset (hC : IsSetSemiring C) (h_ss : ↑I ⊆ C)
(h_dis : PairwiseDisjoint (I : Set (Set α)) id) (ht : t ∈ C) (hJt : ∀ s ∈ I, s ⊆ t) : ∑ u ∈ I, m u ≤ m t := by
classical
rw [addContent_eq_add_disjointOfDiffUnion_of_subset hC ht h_ss hJt h_dis]
exact le_add_right le_rfl
