div_le_div_of_nonneg_right

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

← MathLib Explorer

English

Let a ≤ b and c ≥ 0. Then a/c ≤ b/c.

Русский

Пусть a ≤ b и c ≥ 0. Тогда a/c ≤ b/c.

LaTeX

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

Lean4

@[mono, gcongr, bound]
theorem div_le_div_of_nonneg_right (hab : a ≤ b) (hc : 0 ≤ c) : a / c ≤ b / c :=
  by
  rw [div_eq_mul_inv a c, div_eq_mul_inv b c]
  exact mul_le_mul_of_nonneg_right hab (Right.inv_nonneg.2 hc)

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

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

Разделы

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

Аффилиация

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