div_lt_self

Mathlib.Algebra.Order.Field.Basic

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

English

For a > 0 and b > 1, a/b < a.

Русский

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

LaTeX

$$$ a > 0 \wedge b > 1 \Rightarrow \dfrac{a}{b} < a $$$

Lean4

@[bound]
theorem div_lt_self (ha : 0 < a) (hb : 1 < b) : a / b < a := by
  simpa only [div_one] using div_lt_div_of_pos_left ha zero_lt_one hb

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

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

Разделы

Аффилиация

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