English
Let M be a linearly ordered monoid. For any finite nonempty index set s and function f from the index set to M, the n-th power of the finite supremum of the values f equals the finite supremum of the n-th powers of the values: (max_{i in s} f(i))^n = max_{i in s} (f(i)^n) for every natural n.
Русский
Пусть M — линейно упорядоченная полугруппа. Для любого конечного непустого множества индексов s и функции f: s → M верно: (макcимум по i∈s f(i))^n = максимум по i∈s (f(i))^n для каждого натурального n.
LaTeX
$$$\\forall s \\subseteq I, \\forall f: I \\to M, \\forall n \\in \\mathbb{N}, \\ s \\neq \\emptyset \\implies \\left( \\max_{i \\in s} f(i) \\right)^n = \\max_{i \\in s} \\left( f(i)^n \\right).$$$
Lean4
@[to_additive nsmul_sup']
theorem sup'_pow [LinearOrder M] [Monoid M] [MulLeftMono M] [MulRightMono M] (s : Finset ι) (f : ι → M) (n : ℕ) (hs) :
s.sup' hs f ^ n = s.sup' hs fun a ↦ f a ^ n :=
map_finset_sup' (OrderHom.mk _ <| pow_left_mono n) hs _
