English
In a canonically ordered additive monoid, for any nonempty Finset s and f: s → M and a ∈ M, the equality s.sup' hs f + a = s.sup' hs (i ↦ a + f(i)) holds (up to commutativity, addition order may vary).
Русский
В канонически упорядоченном аддитивном моноиде для любого непустого конечного множества s и функции f: s → M и элемента a: M выполняется равенство s.sup' hs f + a = s.sup' hs (i ↦ a + f(i)).
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} (a + f(i)).$$$
Lean4
/-- Also see `Finset.add_sup'` that works for ordered groups. -/
theorem add_sup'' (hs : s.Nonempty) (f : ι → M) (a : M) : a + s.sup' hs f = s.sup' hs fun i ↦ a + f i := by
simp_rw [add_comm a, Finset.sup'_add']
