div_left — Mathlib

English

If f1 is monovary with g on s and f2 is antivary with g on s, then f1 / f2 is monovary with g on s.

Русский

Если f1 монообразно варьируется с g на s, а f2 антиварируется с g на s, то f1 / f2 варьируется монотонно с g на s.

LaTeX

$$$$\\operatorname{MonovaryOn}(f_1, g, s) \\land \\operatorname{AntivaryOn}(f_2, g, s) \\Rightarrow \\operatorname{MonovaryOn}\\bigl(\\frac{f_1}{f_2}, g, s\\bigr).$$$$

Lean4

@[to_additive]
theorem div_left (h₁ : MonovaryOn f₁ g s) (h₂ : AntivaryOn f₂ g s) : MonovaryOn (f₁ / f₂) g s := fun _i hi _j hj hij ↦
  div_le_div'' (h₁ hi hj hij) (h₂ hi hj hij)

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