inv — Mathlib

English

There is an order-reversing equivalence x ↦ x^{-1} on a group α, i.e., OrderIso.inv: α ≃o αᵒᵈ.

Русский

Существует упорядоченное взаимнооднородное отображение x ↦ x^{-1} на группы α: OrderIso.inv: α ≃o αᵒᵈ.

LaTeX

$$OrderIso.inv : α \simeq o α^{\mathrm{op}}$$

Lean4

/-- `x ↦ x⁻¹` as an order-reversing equivalence. -/
@[to_additive (attr := simps!) /-- `x ↦ -x` as an order-reversing equivalence. -/
    ]
def inv : α ≃o αᵒᵈ where
  toEquiv := (Equiv.inv α).trans OrderDual.toDual
  map_rel_iff' {_ _} := inv_le_inv_iff (α := α)

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