inv_lt_of_inv_lt₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#inv_lt_of_inv_lt₀

English

If a > 0 and a^{-1} < b, then b^{-1} < a.

Русский

Если a > 0 и a^{-1} < b, тогда b^{-1} < a.

LaTeX

$$$0 < a \land a^{-1} < b \Rightarrow b^{-1} < a$$$

Lean4

theorem inv_lt_of_inv_lt₀ (ha : 0 < a) (h : a⁻¹ < b) : b⁻¹ < a :=
  (inv_lt_comm₀ ha <| (inv_pos.2 ha).trans h).1 h

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

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

Разделы

Аффилиация

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