mul_left₀ — Mathlib

English

If hf1, hf2 are nonnegative pointwise, and h1,h2 give AntivaryOn f g on s, then AntivaryOn (f1 * f2) g on s.

Русский

Пусть hf1, hf2 неотрицательны по точкам, и h1,h2 задают 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_left₀ (hf₁ : 0 ≤ f₁) (hf₂ : 0 ≤ f₂) (h₁ : Antivary f₁ g) (h₂ : Antivary f₂ g) : Antivary (f₁ * f₂) g :=
  fun _i _j hij ↦ mul_le_mul (h₁ hij) (h₂ hij) (hf₂ _) (hf₁ _)

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