pow_left₀ — Mathlib

English

If hf is nonnegative on s and hfg is MonovaryOn f g s, then for any n, MonovaryOn f^{n} g s.

Русский

Если hf неотрицателен на s и hfg = MonovaryOn f g s, тогда для любого n имеет место MonovaryOn f^{n} g s.

LaTeX

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

Lean4

theorem pow_left₀ (hf : ∀ i ∈ s, 0 ≤ f i) (hfg : MonovaryOn f g s) (n : ℕ) : MonovaryOn (f ^ n) g s :=
  fun _i hi _j hj hij ↦ pow_le_pow_left₀ (hf _ hi) (hfg hi hj hij) _

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