mul_le_mul_right_of_neg

Mathlib.Algebra.Order.Ring.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#mul_le_mul_right_of_neg

← MathLib Explorer

English

If c < 0, then a*c ≤ b*c is equivalent to b ≤ a for all a,b.

Русский

Если c < 0, то для любых a,b верно a c ≤ b c ↔ b ≤ a.

LaTeX

$$$c < 0 \Rightarrow (a c \le b c \iff b \le a)$$$

Lean4

@[simp]
theorem mul_le_mul_right_of_neg [ExistsAddOfLE R] [MulPosStrictMono R] [AddRightMono R] [AddRightReflectLE R]
    {a b c : R} (h : c < 0) : a * c ≤ b * c ↔ b ≤ a :=
  (strictAnti_mul_right h).le_iff_ge

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru