Units in ordered monoids

instance Units.instPreorder {α : Type u_1} [Monoid α] [Preorder α] : Preorder αˣ

Equations

• Units.instPreorder = Preorder.lift Units.val

instance AddUnits.instPreorder {α : Type u_1} [AddMonoid α] [Preorder α] : Preorder (AddUnits α)

Equations

• AddUnits.instPreorder = Preorder.lift AddUnits.val

@[simp]

theorem Units.val_le_val {α : Type u_1} [Monoid α] [Preorder α] {a b : αˣ} : ↑a ≤ ↑b ↔ a ≤ b

@[simp]

theorem AddUnits.val_le_val {α : Type u_1} [AddMonoid α] [Preorder α] {a b : AddUnits α} : ↑a ≤ ↑b ↔ a ≤ b

@[simp]

theorem Units.val_lt_val {α : Type u_1} [Monoid α] [Preorder α] {a b : αˣ} : ↑a < ↑b ↔ a < b

@[simp]

theorem AddUnits.val_lt_val {α : Type u_1} [AddMonoid α] [Preorder α] {a b : AddUnits α} : ↑a < ↑b ↔ a < b

instance Units.instPartialOrderUnits {α : Type u_1} [Monoid α] [PartialOrder α] : PartialOrder αˣ

Equations

• Units.instPartialOrderUnits = PartialOrder.lift Units.val ⋯

instance AddUnits.instPartialOrderAddUnits {α : Type u_1} [AddMonoid α] [PartialOrder α] : PartialOrder (AddUnits α)

Equations

• AddUnits.instPartialOrderAddUnits = PartialOrder.lift AddUnits.val ⋯

instance Units.instLinearOrder {α : Type u_1} [Monoid α] [LinearOrder α] : LinearOrder αˣ

Equations

• Units.instLinearOrder = LinearOrder.lift' Units.val ⋯

instance AddUnits.instLinearOrder {α : Type u_1} [AddMonoid α] [LinearOrder α] : LinearOrder (AddUnits α)

Equations

• AddUnits.instLinearOrder = LinearOrder.lift' AddUnits.val ⋯

def Units.orderEmbeddingVal {α : Type u_1} [Monoid α] [LinearOrder α] : αˣ ↪o α

val : αˣ → α as an order embedding.

Equations

• Units.orderEmbeddingVal = { toFun := Units.val, inj' := ⋯, map_rel_iff' := ⋯ }

def AddUnits.orderEmbeddingVal {α : Type u_1} [AddMonoid α] [LinearOrder α] : AddUnits α ↪o α

val : add_units α → α as an order embedding.

Equations

• AddUnits.orderEmbeddingVal = { toFun := AddUnits.val, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem AddUnits.orderEmbeddingVal_apply {α : Type u_1} [AddMonoid α] [LinearOrder α] : ⇑AddUnits.orderEmbeddingVal = AddUnits.val

@[simp]

theorem Units.orderEmbeddingVal_apply {α : Type u_1} [Monoid α] [LinearOrder α] : ⇑Units.orderEmbeddingVal = Units.val

@[simp]

theorem Units.max_val {α : Type u_1} [Monoid α] [LinearOrder α] {a b : αˣ} : ↑(a ⊔ b) = ↑a ⊔ ↑b

@[simp]

theorem AddUnits.max_val {α : Type u_1} [AddMonoid α] [LinearOrder α] {a b : AddUnits α} : ↑(a ⊔ b) = ↑a ⊔ ↑b

@[simp]

theorem Units.min_val {α : Type u_1} [Monoid α] [LinearOrder α] {a b : αˣ} : ↑(a ⊓ b) = ↑a ⊓ ↑b

@[simp]

theorem AddUnits.min_val {α : Type u_1} [AddMonoid α] [LinearOrder α] {a b : AddUnits α} : ↑(a ⊓ b) = ↑a ⊓ ↑b