div_le_div_of_nonneg_left

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

← MathLib Explorer

English

If a ≥ 0, c > 0, and c ≤ b, then a/b ≤ a/c.

Русский

Если a ≥ 0, c > 0, и c ≤ b, тогда a/b ≤ a/c.

LaTeX

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

Lean4

theorem div_le_div_of_nonneg_left (ha : 0 ≤ a) (hc : 0 < c) (h : c ≤ b) : a / b ≤ a / c :=
  by
  rw [div_eq_mul_inv, div_eq_mul_inv]
  gcongr
  exacts [ha, hc]

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

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

Разделы

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

Аффилиация

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