pow_right₀ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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