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.

Equations
    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