div_lt_one_of_pos_of_lt

Mathlib.Algebra.Order.Field.Basic

URI: https://scilib.ai/kg/mathlib#Bound.div_lt_one_of_pos_of_lt

English

If b > 0 and a < b, then a/b < 1.

Русский

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

LaTeX

$$$0 < b \\land a < b \\Rightarrow \\dfrac{a}{b} < 1$$$

Lean4

@[bound]
theorem div_lt_one_of_pos_of_lt (b0 : 0 < b) : a < b → a / b < 1 :=
  (div_lt_one b0).mpr

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

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

Разделы

Аффилиация

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