lt_of_mk_lt_mk_of_one_le

Mathlib.Algebra.Order.Archimedean.Class

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

← MathLib Explorer

English

If mk a < mk b and 1 ≤ a, then b < a.

Русский

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

LaTeX

$$mk a < mk b \land 1 \le a \Rightarrow b < a$$

Lean4

@[to_additive]
theorem lt_of_mk_lt_mk_of_one_le (h : mk a < mk b) (hpos : 1 ≤ a) : b < a :=
  by
  obtain h := (mk_lt_mk).mp h 1
  rw [pow_one, mabs_lt, mabs_eq_self.mpr hpos] at h
  exact h.2

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

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

Разделы

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

Аффилиация

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