one_lt_of_one_lt_of_mk_lt

Mathlib.Algebra.Order.Archimedean.Class

URI: https://scilib.ai/kg/mathlib#MulArchimedeanClass.one_lt_of_one_lt_of_mk_lt

← MathLib Explorer

English

If 1 < a and mk a < mk(b / a), then 1 < b.

Русский

Если 1 < a и mk a < mk(b / a), тогда 1 < b.

LaTeX

$$1 < a \land mk a < mk(b / a) \Rightarrow 1 < b$$

Lean4

@[to_additive]
theorem one_lt_of_one_lt_of_mk_lt (ha : 1 < a) (hab : mk a < mk (b / a)) : 1 < b :=
  by
  suffices a⁻¹ < b / a by simpa using this
  apply lt_of_mk_lt_mk_of_le_one
  · simpa using hab
  · simpa using ha.le

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

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

Разделы

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

Аффилиация

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