div_right₀ — Mathlib

English

If similar hypotheses hold as in the previous case, the division by g2 in the previous theorem preserves MonovaryOn on s.

Русский

Если выполняются аналогичные предположения как в предыдущем случае, деление на g2 сохраняет моновариантность на s.

LaTeX

$$$\\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₁ : AntivaryOn f g₁ s)
    (h₂ : MonovaryOn f g₂ s) : AntivaryOn f (g₁ / g₂) s :=
  (h₁.symm.div_left₀ hg₁ hg₂ h₂.symm).symm

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