Units in ordered monoids #
Equations
- AddUnits.instPreorderAddUnits = Preorder.lift AddUnits.val
Equations
- Units.instPreorderUnits = Preorder.lift Units.val
instance
AddUnits.instPartialOrderAddUnits
{α : Type u_1}
[inst : AddMonoid α]
[inst : PartialOrder α]
:
PartialOrder (AddUnits α)
Equations
- AddUnits.instPartialOrderAddUnits = PartialOrder.lift AddUnits.val (_ : Function.Injective fun u => ↑u)
Equations
- Units.instPartialOrderUnits = PartialOrder.lift Units.val (_ : Function.Injective fun u => ↑u)
instance
AddUnits.instLinearOrderAddUnits
{α : Type u_1}
[inst : AddMonoid α]
[inst : LinearOrder α]
:
LinearOrder (AddUnits α)
Equations
- AddUnits.instLinearOrderAddUnits = LinearOrder.lift' AddUnits.val (_ : Function.Injective fun u => ↑u)
Equations
- Units.instLinearOrderUnits = LinearOrder.lift' Units.val (_ : Function.Injective fun u => ↑u)
def
AddUnits.orderEmbeddingVal.proof_1
{α : Type u_1}
[inst : AddMonoid α]
[inst : LinearOrder α]
:
∀ {a b : AddUnits α},
↑{ toFun := AddUnits.val, inj' := (_ : Function.Injective fun u => ↑u) } a ≤ ↑{ toFun := AddUnits.val, inj' := (_ : Function.Injective fun u => ↑u) } b ↔ ↑{ toFun := AddUnits.val, inj' := (_ : Function.Injective fun u => ↑u) } a ≤ ↑{ toFun := AddUnits.val, inj' := (_ : Function.Injective fun u => ↑u) } b
Equations
- One or more equations did not get rendered due to their size.
val : add_units α → α
as an order embedding.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
AddUnits.orderEmbeddingVal_apply
{α : Type u_1}
[inst : AddMonoid α]
[inst : LinearOrder α]
:
↑AddUnits.orderEmbeddingVal.toEmbedding = AddUnits.val
@[simp]
theorem
Units.orderEmbeddingVal_apply
{α : Type u_1}
[inst : Monoid α]
[inst : LinearOrder α]
:
↑Units.orderEmbeddingVal.toEmbedding = Units.val
val : αˣ → α
as an order embedding.
Equations
- One or more equations did not get rendered due to their size.