English
If g1 is nonnegative and g2 is strictly positive on s, MonovaryOn f with g1 and AntivaryOn f with g2 yield MonovaryOn f with g1/g2 on s.
Русский
Если g1 неотрицательная на s, g2 положительна на s, MonovaryOn f с g1 на s и AntivaryOn f с g2 на s дают MonovaryOn 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{MonovaryOn}(f,g_1,s) \\land \\text{AntivaryOn}(f,g_2,s) \\Rightarrow \\text{MonovaryOn}(f,\\tfrac{g_1}{g_2},s)$$$
Lean4
theorem div_right₀ (hg₁ : ∀ i ∈ s, 0 ≤ g₁ i) (hg₂ : ∀ i ∈ s, 0 < g₂ i) (h₁ : MonovaryOn f g₁ s)
(h₂ : AntivaryOn f g₂ s) : MonovaryOn f (g₁ / g₂) s :=
(h₁.symm.div_left₀ hg₁ hg₂ h₂.symm).symm
