div_right — Mathlib

English

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

Русский

Если f моновариантна по отношению к g1 на s и антивариантна по отношению к g2 на s, то f моновариантна по отношению к частному g1/g2 на s.

LaTeX

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

Lean4

@[to_additive]
theorem div_right (h₁ : Monovary f g₁) (h₂ : Antivary f g₂) : Monovary f (g₁ / g₂) := fun _i _j hij ↦
  (lt_or_lt_of_div_lt_div hij).elim (fun h ↦ h₁ h) fun h ↦ h₂ h

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