div_lt_div_right_of_neg

Mathlib.Data.EReal.Inv

URI: https://scilib.ai/kg/mathlib#EReal.div_lt_div_right_of_neg

English

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

Русский

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

LaTeX

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

Lean4

theorem div_lt_div_right_of_neg (h₁ : c < 0) (h₂ : c ≠ ⊥) (h₃ : a < b) : b / c < a / c :=
  strictAnti_div_right_of_neg h₁ h₂ h₃

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

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

Разделы

Аффилиация

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