div_le_div_iff_of_pos_left

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

← MathLib Explorer

English

For a,b,c > 0, a/b ≤ a/c iff c ≤ b.

Русский

Для a,b,c > 0, a/b ≤ a/c эквивалентно c ≤ b.

LaTeX

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

Lean4

theorem div_le_div_iff_of_pos_left (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a / b ≤ a / c ↔ c ≤ b := by
  simp only [div_eq_mul_inv, mul_le_mul_iff_right₀ ha, inv_le_inv₀ hb hc]

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

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

Разделы

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

Аффилиация

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