pow_right₀ — Mathlib

English

If hg is nonnegative on s and hfg is AntivaryOn f g on s, then for all n, AntivaryOn f (g^n) s.

Русский

Если hg неотрицателен на s и hfg = AntivaryOn f g s, тогда для любого n AntivaryOn f (g^n) s.

LaTeX

$$$ (\forall i \in s, 0 \le g(i)) \Rightarrow AntivaryOn f g s \Rightarrow \forall n, AntivaryOn f (g^n) s $$$

Lean4

theorem pow_right₀ (hg : ∀ i ∈ s, 0 ≤ g i) (hfg : AntivaryOn f g s) (n : ℕ) : AntivaryOn f (g ^ n) s :=
  (hfg.symm.pow_left₀ hg _).symm

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