inv_Ioi — Mathlib

English

In any ordered commutative group, inversion x ↦ x^{-1} reverses the order on rays: the image of the open interval (a, ∞) under inversion is the open interval (−∞, a^{-1}). Equivalently, (Ioi a)^{-1} = Iio a^{-1}.

Русский

В упорядоченной коммутативной группе преобразование в обратное x ↦ x^{-1} обращает порядок на лучах: образ открытого полуотрезка (a, ∞) при взятии обратного равен открытому лучу (−∞, a^{-1}). То есть (Ioi a)^{-1} = Iio a^{-1}.

LaTeX

$$$$(Ioi\\ a)^{-1} = Iio\\ a^{-1}$$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_Ioi (a : α) : (Ioi a)⁻¹ = Iio a⁻¹ :=
  ext fun _x ↦ lt_inv'

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