one_lt_div_of_pos_of_lt

Mathlib.Algebra.Order.Field.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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