div_lt_div_of_pos_left

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$0 < a \land 0 < c \land c < b \Rightarrow \frac{a}{b} < \frac{a}{c}$$$

Lean4

@[gcongr, bound]
theorem div_lt_div_of_pos_left (ha : 0 < a) (hc : 0 < c) (h : c < b) : a / b < a / c :=
  (div_lt_div_iff_of_pos_left ha (hc.trans h) hc).mpr h

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

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

Разделы

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

Аффилиация

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