mul_right₀ — Mathlib

English

Let g1,g2 be nonnegative functions on s; if Antivary f g1 s and Antivary f g2 s, then Antivary f (g1 * g2) s.

Русский

Пусть g1 и g2 неотрицательны на s и Antivary f g1 s, Antivary f g2 s. Тогда Antivary f (g1 g2) s.

LaTeX

$$$ (\forall i \in s, 0 ≤ g_1(i)) \land (\forall i \in s, 0 ≤ g_2(i)) \land AntivaryOn f g_1 s \land AntivaryOn f g_2 s \Rightarrow AntivaryOn f (g_1 g_2) s $$$

Lean4

theorem mul_right₀ (hg₁ : 0 ≤ g₁) (hg₂ : 0 ≤ g₂) (h₁ : Antivary f g₁) (h₂ : Antivary f g₂) : Antivary f (g₁ * g₂) :=
  (h₁.symm.mul_left₀ hg₁ hg₂ h₂.symm).symm

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