mul_right₀ — Mathlib

English

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

Русский

Если hf неотрицателен на s и 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 mul_right₀ (hg₁ : ∀ i ∈ s, 0 ≤ g₁ i) (hg₂ : ∀ i ∈ s, 0 ≤ g₂ i) (h₁ : MonovaryOn f g₁ s)
    (h₂ : MonovaryOn f g₂ s) : MonovaryOn f (g₁ * g₂) s :=
  (h₁.symm.mul_left₀ hg₁ hg₂ h₂.symm).symm

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