English
Under nonnegativity and positivity assumptions on f1 and f2, MonovaryOn f1 g on s together with AntivaryOn f2 g on s imply MonovaryOn (f1/f2) g on s.
Русский
При неотрицательности и положительности на f1 и f2, 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) \\land \\bigl(\\forall i \\in s,\\ 0 < f_2(i)\\bigr) \\land \\text{MonovaryOn}(f_1,g,s) \\land \\text{AntivaryOn}(f_2,g,s) \\Rightarrow \\text{MonovaryOn}\\left(\\frac{f_1}{f_2},g,s\\right)$$$
Lean4
theorem div_right₀ (hg₁ : 0 ≤ g₁) (hg₂ : StrongLT 0 g₂) (h₁ : Monovary f g₁) (h₂ : Antivary f g₂) :
Monovary f (g₁ / g₂) :=
(h₁.symm.div_left₀ hg₁ hg₂ h₂.symm).symm
