coe_orderIso — Mathlib

English

The underlying function of an ordered monoid isomorphism, when viewed as an order isomorphism, is the same as the map itself.

Русский

Левая функция упорядоченного моноидного изоморфизма, когда её рассматривать как изоморфизм порядка, совпадает с самой картой.

LaTeX

$$$((f : α \simeq^*o β) : α \too β) = f$.$$

Lean4

@[to_additive (attr := simp)]
theorem coe_orderIso (f : α ≃*o β) : ((f : α →o β) : α → β) = f :=
  rfl

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