symm — Mathlib

English

The inverse of an order monoid iso is an order monoid iso.

Русский

Обратный к упорядоченному моноидному изоморфизму есть упорядоченный моноидный изоморфизм.

LaTeX

$$def symm (f : α \simeq^*o β) : β \simeq^*o α := ⟨f.toMulEquiv.symm, f.toOrderIso.symm.map_rel_iff⟩$$

Lean4

/-- The inverse of an isomorphism is an isomorphism. -/
@[to_additive (attr := symm) /-- The inverse of an order isomorphism is an order isomorphism. -/
    ]
def symm (f : α ≃*o β) : β ≃*o α :=
  ⟨f.toMulEquiv.symm, f.toOrderIso.symm.map_rel_iff⟩

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