English
If hf1 and hf2 assert nonnegativity of f1 and f2 on s, and h1,h2 give AntivaryOn f1 g and AntivaryOn f2 g on s, then AntivaryOn (f1 * f2) g on s.
Русский
Пусть hf1 и hf2 задают неотрицательность f1 и f2 на s, а h1 и h2 задают AntivaryOn f1 g s и AntivaryOn f2 g s. Тогда AntivaryOn (f1 * f2) g s.
LaTeX
$$$ (\forall i \in s, 0 \le f_1(i)) \land (\forall i \in s, 0 \le f_2(i)) \land AntivaryOn f_1 g s \land AntivaryOn f_2 g s \Rightarrow AntivaryOn (f_1 f_2) g s $$$
Lean4
theorem mul_left₀ (hf₁ : ∀ i ∈ s, 0 ≤ f₁ i) (hf₂ : ∀ i ∈ s, 0 ≤ f₂ i) (h₁ : AntivaryOn f₁ g s)
(h₂ : AntivaryOn f₂ g s) : AntivaryOn (f₁ * f₂) g s := fun _i hi _j hj hij ↦
mul_le_mul (h₁ hi hj hij) (h₂ hi hj hij) (hf₂ _ hj) (hf₁ _ hi)
