mul_right₀ — Mathlib

English

If hf1 hv hf2 hold nonnegativity of f1 and f2 on s and AntivaryOn f g on s and AntivaryOn f g on s, then AntivaryOn (f1 * f2) g on s.

Русский

Пусть hf1, hf2 задают неотрицательность f1 и f2 на s, AntivaryOn f g на s; тогда AntivaryOn (f1 * f2) g на s.

LaTeX

$$$ (\forall i, 0 \le f_1(i)) \land (\forall i, 0 \le f_2(i)) \land AntivaryOn f g s \land AntivaryOn f g s \Rightarrow AntivaryOn (f_1 f_2) g s $$$

Lean4

theorem mul_right₀ (hg₁ : ∀ i ∈ s, 0 ≤ g₁ i) (hg₂ : ∀ i ∈ s, 0 ≤ g₂ i) (h₁ : AntivaryOn f g₁ s)
    (h₂ : AntivaryOn f g₂ s) : AntivaryOn f (g₁ * g₂) s :=
  (h₁.symm.mul_left₀ hg₁ hg₂ h₂.symm).symm

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