Units in ordered monoids #

source

ink

instance AddUnits.instPreorderAddUnits {α : Type u_1} [inst : AddMonoid α] [inst : Preorder α] :

Preorder (AddUnits α)

Equations

AddUnits.instPreorderAddUnits = Preorder.lift AddUnits.val

source

ink

instance Units.instPreorderUnits {α : Type u_1} [inst : Monoid α] [inst : Preorder α] :

Preorder αˣ

Equations

Units.instPreorderUnits = Preorder.lift Units.val

source

ink

@[simp]

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

↑a ≤ ↑b ↔ a ≤ b

source

ink

@[simp]

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

↑a ≤ ↑b ↔ a ≤ b

source

ink

@[simp]

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

↑a < ↑b ↔ a < b

source

ink

@[simp]

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

↑a < ↑b ↔ a < b

source

ink

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

PartialOrder (AddUnits α)

Equations

AddUnits.instPartialOrderAddUnits = PartialOrder.lift AddUnits.val (_ : Function.Injective fun u => ↑u)

source

ink

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

PartialOrder αˣ

Equations

Units.instPartialOrderUnits = PartialOrder.lift Units.val (_ : Function.Injective fun u => ↑u)

source

ink

instance AddUnits.instLinearOrderAddUnits {α : Type u_1} [inst : AddMonoid α] [inst : LinearOrder α] :

LinearOrder (AddUnits α)

Equations

AddUnits.instLinearOrderAddUnits = LinearOrder.lift' AddUnits.val (_ : Function.Injective fun u => ↑u)

source

ink

instance Units.instLinearOrderUnits {α : Type u_1} [inst : Monoid α] [inst : LinearOrder α] :

LinearOrder αˣ

Equations

Units.instLinearOrderUnits = LinearOrder.lift' Units.val (_ : Function.Injective fun u => ↑u)

source

ink

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.

source

ink

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

AddUnits α ↪o α

val : add_units α → α as an order embedding.

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem AddUnits.orderEmbeddingVal_apply {α : Type u_1} [inst : AddMonoid α] [inst : LinearOrder α] :

↑AddUnits.orderEmbeddingVal.toEmbedding = AddUnits.val

source

ink

@[simp]

theorem Units.orderEmbeddingVal_apply {α : Type u_1} [inst : Monoid α] [inst : LinearOrder α] :

↑Units.orderEmbeddingVal.toEmbedding = Units.val

source

ink

def Units.orderEmbeddingVal {α : Type u_1} [inst : Monoid α] [inst : LinearOrder α] :

αˣ ↪o α

val : αˣ → α as an order embedding.

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem AddUnits.max_val {α : Type u_1} [inst : AddMonoid α] [inst : LinearOrder α] {a : AddUnits α} {b : AddUnits α} :

↑(max a b) = max ↑a ↑b

source

ink

@[simp]

theorem Units.max_val {α : Type u_1} [inst : Monoid α] [inst : LinearOrder α] {a : αˣ} {b : αˣ} :

↑(max a b) = max ↑a ↑b

source

ink

@[simp]

theorem AddUnits.min_val {α : Type u_1} [inst : AddMonoid α] [inst : LinearOrder α] {a : AddUnits α} {b : AddUnits α} :

↑(min a b) = min ↑a ↑b

source

ink

@[simp]

theorem Units.min_val {α : Type u_1} [inst : Monoid α] [inst : LinearOrder α] {a : αˣ} {b : αˣ} :

↑(min a b) = min ↑a ↑b