div_le_self

Mathlib.Algebra.Order.Field.Basic

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

English

For a ≥ 0 and b ≥ 1, a/b ≤ a.

Русский

Если a ≥ 0 и b ≥ 1, то a/b ≤ a.

LaTeX

$$$ a \ge 0 \wedge b \ge 1 \Rightarrow \dfrac{a}{b} \le a $$$

Lean4

@[bound]
theorem div_le_self (ha : 0 ≤ a) (hb : 1 ≤ b) : a / b ≤ a := by
  simpa only [div_one] using div_le_div_of_nonneg_left ha zero_lt_one hb

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

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

Разделы

Аффилиация

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