English
Let M be an AddCommMonoid with linear order and canonically ordered addition. For any nonempty finite s and f: s → M and a ∈ M, we have s.sup' hs f + a = s.sup' hs (i ↦ f(i) + a).
Русский
Пусть M — добавочное коммутативное моноид с линейным порядком и канонически упорядоченным сложением. Тогда для любого непустого конечного s и функции f: s → M верно: s.sup' hs f + a = s.sup' hs (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
/-- Also see `Finset.sup'_add` that works for ordered groups. -/
theorem sup'_add' (s : Finset ι) (f : ι → M) (a : M) (hs : s.Nonempty) : s.sup' hs f + a = s.sup' hs fun i ↦ f i + a :=
by
apply le_antisymm
· apply add_le_of_le_tsub_right_of_le
· exact Finset.le_sup'_of_le _ hs.choose_spec le_add_self
· exact Finset.sup'_le _ _ fun i hi ↦ le_tsub_of_add_le_right (Finset.le_sup' (f · + a) hi)
· exact Finset.sup'_le _ _ fun i hi ↦ add_le_add_right (Finset.le_sup' _ hi) _
