English
Let M be an AddCommMonoid with LinearOrder and OrderBot. Then for any nonempty Finset s, function f: s → M and a ∈ M, we have s.sup f + a = s.sup (i ↦ f(i) + a).
Русский
Пусть M — коммутативный аддитивный моноид с линейным порядком и нулем-подобной нижней степенью. Тогда для любого непустого Finset s и функции f: s → M выполняется s.sup f + a = s.sup (i ↦ f(i) + a).
LaTeX
$$$\\forall s:\\ Finset\\, I, \\forall f: I \\to M, \\forall a:\\ M, \\ s.Nonempty \\implies \\left( \\sup_{i\\in s} f(i) \\right) + a = \\sup_{i\\in s} (f(i) + a).$$$
Lean4
protected theorem sup_add (hs : s.Nonempty) (f : ι → M) (a : M) : s.sup f + a = s.sup fun i ↦ f i + a := by
rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_add']
