div_left₀ — Mathlib

English

If f1 is nonnegative and f2 is strictly negative near zero, Antivary f1 with g and Monovary f2 with g imply Antivary (f1/f2) with g.

Русский

Если f1 неотрицательна и f2 строго меньше нуля около нуля, Antivary f1 с g и Monovary f2 с g дают Antivary (f1/f2) с g.

LaTeX

$$$\\bigl(0 \\le f_1\\bigr) \\land \\text{StrongLT }0 f_2 \\land \\text{AntivaryOn }f_1 g \\land \\text{MonovaryOn }f_2 g \\Rightarrow \\text{AntivaryOn}\\left(\\frac{f_1}{f_2},g\\right)$$$

Lean4

theorem div_left₀ (hf₁ : 0 ≤ f₁) (hf₂ : StrongLT 0 f₂) (h₁ : Antivary f₁ g) (h₂ : Monovary f₂ g) :
    Antivary (f₁ / f₂) g := fun _i _j hij ↦ div_le_div₀ (hf₁ _) (h₁ hij) (hf₂ _) <| h₂ hij

Похожие утверждения