pow_left₀ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem pow_left₀ (hf : 0 ≤ f) (hfg : Antivary f g) (n : ℕ) : Antivary (f ^ n) g := fun _i _j hij ↦
  pow_le_pow_left₀ (hf _) (hfg hij) _

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