English
If for all i in s we have f1(i) ≥ 0 and f2(i) > 0, AntivaryOn f1 with g on s and MonovaryOn f2 with g on s yield AntivaryOn (f1/f2) with g on s.
Русский
Если для всех i ∈ s выполняется f1(i) ≥ 0 и f2(i) > 0, AntivaryOn f1 с g на s и MonovaryOn f2 с g на s дают AntivaryOn (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{AntivaryOn}(f_1,g,s) \\rightarrow \\text{MonovaryOn}(f_2,g,s) \\rightarrow \\text{AntivaryOn}\\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₁ : AntivaryOn f₁ g s)
(h₂ : MonovaryOn f₂ g s) : AntivaryOn (f₁ / f₂) g s := fun _i hi _j hj hij ↦
div_le_div₀ (hf₁ _ hi) (h₁ hi hj hij) (hf₂ _ hi) <| h₂ hi hj hij
