English
For a function f from a lattice to an ordered additive monoid, the value at a finite supremum is bounded by the finite sum over components: f(t.sup s) ≤ ∑_{i∈t} f(s(i)).
Русский
Для функции из латки в упорядоченную аддитивную моноиду, значение в конечном верхнем пределe ограничено суммой по компонентам: f(t.sup s) ≤ ∑_{i∈t} f(s(i)).
LaTeX
$$$f(\,t \;\text{sup}\; s) \le \sum_{i \in t} f(s(i))$$$
Lean4
theorem apply_sup_le_sum [SemilatticeSup α] [OrderBot α] [AddCommMonoid β] [PartialOrder β] [AddLeftMono β] {f : α → β}
(zero : f ⊥ = 0) (ih : ∀ {s t}, f (s ⊔ t) ≤ f s + f t) {s : ι → α} (t : Finset ι) :
f (t.sup s) ≤ ∑ i ∈ t, f (s i) := by
classical
refine t.induction_on zero.le fun i t it h ↦ ?_
simpa only [sup_insert, Finset.sum_insert it] using ih.trans (by gcongr)
