div_right — Mathlib

English

If f antivaries with g1 on s and monovaries with g2 on s, then f antivaries with g1/g2 on s.

Русский

Пусть f антивариантна по отношению к g1 на s и моновариантна по отношению к g2 на s. Тогда f антивариантна по отношению к частному g1/g2 на s.

LaTeX

$$$ AntivaryOn f g_1 s \land MonovaryOn f g_2 s \Rightarrow AntivaryOn f \bigl( \dfrac{g_1}{g_2} \bigr) s $$$

Lean4

@[to_additive]
theorem div_right (h₁ : AntivaryOn f g₁ s) (h₂ : MonovaryOn f g₂ s) : AntivaryOn f (g₁ / g₂) s := fun _i hi _j hj hij ↦
  (lt_or_lt_of_div_lt_div hij).elim (h₁ hi hj) <| h₂ hj hi

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