div_lt_div_of_neg_of_lt

Mathlib.Algebra.Order.Field.Basic

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

← MathLib Explorer

English

If c < 0 and b < a, then a/c < b/c.

Русский

Если c < 0 и b < a, то a/c < b/c.

LaTeX

$$$(c < 0) \land (b < a) \Rightarrow a/c < b/c$$$

Lean4

theorem div_lt_div_of_neg_of_lt (hc : c < 0) (h : b < a) : a / c < b / c :=
  by
  rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c]
  exact mul_lt_mul_of_neg_right h (one_div_neg.2 hc)

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

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

Разделы

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

Аффилиация

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