English
Let f: I → A and g: I → B be functions into linearly ordered sets A and B with g nonnegative at every point, and suppose f and g are in a monotone-variation relation (monovary). Then for every natural exponent n, f is in the same monotone-variation relation with g^n.
Русский
Пусть f: I → A и g: I → B — функции в линейно упорядоченные множества A и B, причём g неотрицательно на каждом элементе, и пусть f и g образуют моно-вариантность (monovary). Тогда для каждого натурального n выполняется, что f и g^n образуют ту же моно-вариантность.
LaTeX
$$$\\left(\\forall i,\, 0 \\le g(i)\\right) \\land \\text{Monovary}(f,g) \\Rightarrow \\forall n \\in \\mathbb{N},\\; \\text{Monovary}(f,g^n)$$$
Lean4
theorem pow_right₀ (hg : 0 ≤ g) (hfg : Monovary f g) (n : ℕ) : Monovary f (g ^ n) :=
(hfg.symm.pow_left₀ hg _).symm
