English
Let M be a linearly ordered group. For any nonempty finite s and f: s → M and any a ∈ M, the right multiplication distributes over the finite supremum: (sup' f)·a = sup' (i ↦ f(i)·a).
Русский
Пусть M - линейно упорядоченная группа. Для любом непустого конечного множества s и функции f: s → M и элемента a ∈ M выполняется: (sup' f)·a = sup' (i ↦ f(i)·a).
LaTeX
$$$\\forall s:\\ Finset\\, I, \\forall f: I \\to G, \\forall a:\\ G, \\ s.Nonempty \\implies \\left( \\sup_{i\\in s} f(i) \\right) \\cdot a = \\sup_{i\\in s} \\left( f(i) \\cdot a \\right).$$$
Lean4
@[to_additive /-- Also see `Finset.sup'_add'` that works for canonically ordered monoids. -/
]
theorem sup'_mul [MulRightMono G] (s : Finset ι) (f : ι → G) (a : G) (hs) :
s.sup' hs f * a = s.sup' hs fun i ↦ f i * a :=
map_finset_sup' (OrderIso.mulRight a) hs f
