invOrderIso — Mathlib

English

Pointwise inversion of submonoids is an order isomorphism: Submonoid invOrderIso maps S to S⁻¹ preserving and reflecting the order.

Русский

Поэлементная инверсия подмономоидов является упорядоченным изomорфизмом: invOrderIso отображает S в S⁻¹ и сохраняет/отражает порядок.

LaTeX

$$$\\text{invOrderIso} : \\text{submonoid } G \\cong_o \\text{submonoid } G$$$

Lean4

/-- Pointwise inversion of submonoids as an order isomorphism. -/
@[to_additive (attr := simps!) /-- Pointwise negation of additive submonoids as an order isomorphism -/
    ]
def invOrderIso : Submonoid G ≃o Submonoid G where
  toEquiv := Equiv.inv _
  map_rel_iff' := inv_le_inv _ _

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