English
Let G be a linearly ordered group with left-multiplication mono. For any nonempty finite s and f: s → G and a ∈ G, we have a · (sup' f) = sup'(i ↦ a · f(i)).
Русский
Пусть G — линейно упорядоченная группа, у которой левая умножение сохраняет неубывание. Тогда, для непустого конечного s и f: s → G, для любого a: G выполняется a·(sup' f) = sup'(i ↦ a·f(i)).
LaTeX
$$$\\forall s:\\ Finset\\, I, \\forall f: I \\to G, \\forall a:\\ G, \\ s.Nonempty \\implies a \\cdot \\left( \\sup_{i\\in s} f(i) \\right) = \\sup_{i\\in s} (a \\cdot f(i)).$$$
Lean4
@[to_additive /-- Also see `Finset.add_sup''` that works for canonically ordered monoids. -/
]
theorem mul_sup' [MulLeftMono G] (s : Finset ι) (f : ι → G) (a : G) (hs) :
a * s.sup' hs f = s.sup' hs fun i ↦ a * f i :=
map_finset_sup' (OrderIso.mulLeft a) hs f
