Isomorphism of submonoids of ordered monoids

def Submonoid.topOrderMonoidIso {α : Type u_1} [Preorder α] [Monoid α] : ↥⊤ ≃*o α

The top submonoid is order isomorphic to the whole monoid.

Equations

• Submonoid.topOrderMonoidIso = { toMulEquiv := Submonoid.topEquiv, map_le_map_iff' := ⋯ }

@[simp]

theorem Submonoid.topOrderMonoidIso_symm_apply_coe {α : Type u_1} [Preorder α] [Monoid α] (x : α) : ↑(topOrderMonoidIso.symm x) = x

@[simp]

theorem Submonoid.topOrderMonoidIso_apply {α : Type u_1} [Preorder α] [Monoid α] (x : ↥⊤) : topOrderMonoidIso x = ↑x