English
If for all i in s we have f1(i) ≥ 0 and f2(i) > 0, and MonovaryOn f1 with g on s while AntivaryOn f2 with g on s, then MonovaryOn (f1/f2) with g on s.
Русский
Если для всех i ∈ s выполняется f1(i) ≥ 0 и f2(i) > 0, и MonovaryOn f1 с g на s, а AntivaryOn f2 с g на s, тогда MonovaryOn (f1/f2) с g на s.
LaTeX
$$$\\bigl(\\forall i \\in s,\\; 0 \\le f_1(i)\\bigr) \\rightarrow\\bigl(\\forall i \\in s,\\; 0 < f_2(i)\\bigr) \\rightarrow\\text{MonovaryOn}(f_1,g,s) \\rightarrow \\text{AntivaryOn}(f_2,g,s) \\rightarrow \\text{MonovaryOn}\\left(\\frac{f_1}{f_2},g,s\\right)$$$
Lean4
theorem div_left₀ (hf₁ : ∀ i ∈ s, 0 ≤ f₁ i) (hf₂ : ∀ i ∈ s, 0 < f₂ i) (h₁ : MonovaryOn f₁ g s)
(h₂ : AntivaryOn f₂ g s) : MonovaryOn (f₁ / f₂) g s := fun _i hi _j hj hij ↦
div_le_div₀ (hf₁ _ hj) (h₁ hi hj hij) (hf₂ _ hj) <| h₂ hi hj hij
