div_lt_div_right_of_pos

Mathlib.Data.EReal.Inv

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

English

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

Русский

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

LaTeX

$$$0 < c \land c \neq \top \land a < b \Rightarrow a / c < b / c$$$

Lean4

@[gcongr]
theorem div_lt_div_right_of_pos (h₁ : 0 < c) (h₂ : c ≠ ⊤) (h₃ : a < b) : a / c < b / c :=
  strictMono_div_right_of_pos h₁ h₂ h₃

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

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

Разделы

Аффилиация

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