English
If g1 is nonnegative and g2 is strictly positive on s, AntivaryOn f with g1 and MonovaryOn f with g2 yield AntivaryOn f (g1/g2) on s.
Русский
Если g1 неотрицательная и g2 строго положительная на s, AntivaryOn f с g1 и MonovaryOn f с g2 дают AntivaryOn f (g1/g2) на s.
LaTeX
$$$\\bigl(\\forall i \\in s,\\ 0 \\le g_1(i)\\bigr) \\land \\bigl(\\forall i \\in s,\\ 0 < g_2(i)\\bigr) \\land \\text{AntivaryOn}(f,g_1,s) \\land \\text{MonovaryOn}(f,g_2,s) \\Rightarrow \\text{AntivaryOn}\\left(f,\\tfrac{g_1}{g_2},s\\right)$$$
Lean4
theorem div_right₀ (hg₁ : 0 ≤ g₁) (hg₂ : StrongLT 0 g₂) (h₁ : Antivary f g₁) (h₂ : Monovary f g₂) :
Antivary f (g₁ / g₂) :=
(h₁.symm.div_left₀ hg₁ hg₂ h₂.symm).symm
