inv_pos — Mathlib

English

In a group with zero equipped with a compatible order, an element is positive if and only if its inverse is positive.

Русский

В группе с нулём, снабжённой совместимым порядком, элемент положителен тогда и только тогда, когда его обратный элемент положителен.

LaTeX

$$$0 < a^{-1} \iff 0 < a$$$

Lean4

theorem inv_pos : 0 < a⁻¹ ↔ 0 < a :=
  by
  suffices ∀ a : G₀, 0 < a → 0 < a⁻¹ from ⟨fun h ↦ inv_inv a ▸ this _ h, this a⟩
  intro a ha
  apply lt_of_mul_lt_mul_right _ ha.le
  apply lt_of_mul_lt_mul_right _ ha.le
  simpa [ha.ne']

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