div_left₀ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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