Documentation

Mathlib.Algebra.Order.Hom.Submonoid

Isomorphism of submonoids of ordered monoids #

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

The top submonoid is order isomorphic to the whole monoid.

Instances For
    source
    📐 coverage
    @[simp]
    theorem Submonoid.topOrderMonoidIso_symm_apply_coe {α : Type u_1} [Preorder α] [Monoid α] (x : α) :
    ↑(topOrderMonoidIso.symm x) = x
    source
    📐 coverage
    @[simp]
    theorem Submonoid.topOrderMonoidIso_apply {α : Type u_1} [Preorder α] [Monoid α] (x : ↥⊤) :
    topOrderMonoidIso x = ↑x