English
If hC is a SetSemiring and s ≤ t with s,t ∈ C, then m(s) ≤ m(t). This follows from the previous sum lemma by considering the singleton subset.
Русский
Если hC — множество полуполей и s ≤ t с s,t ∈ C, то m(s) ≤ m(t). Это следует из предыдущего леммы сумм, применённой к одиночному элементу.
LaTeX
$$$$ \\text{If } hC:\\ IsSetSemiring\\, C, \\; s,t \\in C, \\; s \\subseteq t, \\; \\Rightarrow m(s) \\le m(t). $$$$
Lean4
/-- An `addContent C` on a `SetSemiring C` is monotone. -/
theorem addContent_mono (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) (hst : s ⊆ t) : m s ≤ m t :=
by
have h := sum_addContent_le_of_subset (m := m) hC (I := { s }) ?_ ?_ ht ?_
· simpa only [sum_singleton] using h
· rwa [singleton_subset_set_iff]
· simp only [coe_singleton, pairwiseDisjoint_singleton]
· simp [hst]
