English
If hf1, hf2 give nonnegativity of f1,f2 on s, and h1,h2 give MonovaryOn f1 g and MonovaryOn f2 g on s, then MonovaryOn (f1 * f2) g on s.
Русский
Пусть hf1, hf2 обеспечивают неотрицательность f1, f2 на s, а h1, h2 задают MonovaryOn f1 g s и MonovaryOn f2 g s. Тогда MonovaryOn (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 MonovaryOn f_1 g s \land MonovaryOn f_2 g s \Rightarrow MonovaryOn (f_1 f_2) g s $$$
Lean4
theorem mul_left₀ (hf₁ : ∀ i ∈ s, 0 ≤ f₁ i) (hf₂ : ∀ i ∈ s, 0 ≤ f₂ i) (h₁ : MonovaryOn f₁ g s)
(h₂ : MonovaryOn f₂ g s) : MonovaryOn (f₁ * f₂) g s := fun _i hi _j hj hij ↦
mul_le_mul (h₁ hi hj hij) (h₂ hi hj hij) (hf₂ _ hi) (hf₁ _ hj)
