pow_right₀ — Mathlib

English

Let f: I → A and g: I → B be functions with g nonnegative everywhere, and suppose f and g are antivary. Then for every natural exponent n, f is antivary with respect to g^n.

Русский

Пусть f: I → A и g: I → B — функции, для которых g неотрицательно на всей области определения, и пусть f и g образуют antivary. Тогда для каждого натурального n f и g^n образуют antivary.

LaTeX

$$$\\left(\\forall i,\, 0 \\le g(i)\\right) \\land \\text{Antivary}(f,g) \\Rightarrow \\forall n \\in \\mathbb{N},\\; \\text{Antivary}(f,g^n)$$$

Lean4

theorem pow_right₀ (hg : 0 ≤ g) (hfg : Antivary f g) (n : ℕ) : Antivary f (g ^ n) :=
  (hfg.symm.pow_left₀ hg _).symm

Похожие утверждения