lt_inv_of_neg — Mathlib

English

Let a and b be elements of an ordered field with a linear order, and assume a < 0 and b < 0. Then a is less than the reciprocal of b if and only if b is less than the reciprocal of a.

Русский

Пусть a и b — элементы упорядоченного поля, причём a < 0 и b < 0. Тогда a < b^{-1} тогда же ∀ и только если b < a^{-1}.

LaTeX

$$$\,(a<0 \land b<0) \Rightarrow (a < b^{-1} \iff b < a^{-1})\,$$$

Lean4

theorem lt_inv_of_neg (ha : a < 0) (hb : b < 0) : a < b⁻¹ ↔ b < a⁻¹ :=
  lt_iff_lt_of_le_iff_le (inv_le_of_neg hb ha)

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