# Documentation

Mathlib.Algebra.Order.Monoid.OrderDual

# Ordered monoid structures on the order dual. #

def OrderDual.contravariantClass_add_le.proof_1 {α : Type u_1} [inst : LE α] [inst : Add α] [c : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] :
ContravariantClass αᵒᵈ αᵒᵈ (fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
instance OrderDual.contravariantClass_add_le {α : Type u} [inst : LE α] [inst : Add α] [c : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] :
ContravariantClass αᵒᵈ αᵒᵈ (fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
instance OrderDual.contravariantClass_mul_le {α : Type u} [inst : LE α] [inst : Mul α] [c : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] :
ContravariantClass αᵒᵈ αᵒᵈ (fun x x_1 => x * x_1) fun x x_1 => x x_1
Equations
instance OrderDual.covariantClass_add_le {α : Type u} [inst : LE α] [inst : Add α] [c : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] :
CovariantClass αᵒᵈ αᵒᵈ (fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
def OrderDual.covariantClass_add_le.proof_1 {α : Type u_1} [inst : LE α] [inst : Add α] [c : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] :
CovariantClass αᵒᵈ αᵒᵈ (fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
instance OrderDual.covariantClass_mul_le {α : Type u} [inst : LE α] [inst : Mul α] [c : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] :
CovariantClass αᵒᵈ αᵒᵈ (fun x x_1 => x * x_1) fun x x_1 => x x_1
Equations
instance OrderDual.contravariantClass_swap_add_le {α : Type u} [inst : LE α] [inst : Add α] [c : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] :
ContravariantClass αᵒᵈ αᵒᵈ (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
def OrderDual.contravariantClass_swap_add_le.proof_1 {α : Type u_1} [inst : LE α] [inst : Add α] [c : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] :
ContravariantClass αᵒᵈ αᵒᵈ (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
instance OrderDual.contravariantClass_swap_mul_le {α : Type u} [inst : LE α] [inst : Mul α] [c : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] :
ContravariantClass αᵒᵈ αᵒᵈ (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1
Equations
instance OrderDual.covariantClass_swap_add_le {α : Type u} [inst : LE α] [inst : Add α] [c : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] :
CovariantClass αᵒᵈ αᵒᵈ (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
def OrderDual.covariantClass_swap_add_le.proof_1 {α : Type u_1} [inst : LE α] [inst : Add α] [c : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] :
CovariantClass αᵒᵈ αᵒᵈ (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1
Equations
instance OrderDual.covariantClass_swap_mul_le {α : Type u} [inst : LE α] [inst : Mul α] [c : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] :
CovariantClass αᵒᵈ αᵒᵈ (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1
Equations
instance OrderDual.contravariantClass_add_lt {α : Type u} [inst : LT α] [inst : Add α] [c : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
ContravariantClass αᵒᵈ αᵒᵈ (fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
def OrderDual.contravariantClass_add_lt.proof_1 {α : Type u_1} [inst : LT α] [inst : Add α] [c : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
ContravariantClass αᵒᵈ αᵒᵈ (fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
instance OrderDual.contravariantClass_mul_lt {α : Type u} [inst : LT α] [inst : Mul α] [c : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] :
ContravariantClass αᵒᵈ αᵒᵈ (fun x x_1 => x * x_1) fun x x_1 => x < x_1
Equations
instance OrderDual.covariantClass_add_lt {α : Type u} [inst : LT α] [inst : Add α] [c : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
CovariantClass αᵒᵈ αᵒᵈ (fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
def OrderDual.covariantClass_add_lt.proof_1 {α : Type u_1} [inst : LT α] [inst : Add α] [c : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
CovariantClass αᵒᵈ αᵒᵈ (fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
instance OrderDual.covariantClass_mul_lt {α : Type u} [inst : LT α] [inst : Mul α] [c : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] :
CovariantClass αᵒᵈ αᵒᵈ (fun x x_1 => x * x_1) fun x x_1 => x < x_1
Equations
instance OrderDual.contravariantClass_swap_add_lt {α : Type u} [inst : LT α] [inst : Add α] [c : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
ContravariantClass αᵒᵈ αᵒᵈ (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
def OrderDual.contravariantClass_swap_add_lt.proof_1 {α : Type u_1} [inst : LT α] [inst : Add α] [c : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
ContravariantClass αᵒᵈ αᵒᵈ (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
instance OrderDual.contravariantClass_swap_mul_lt {α : Type u} [inst : LT α] [inst : Mul α] [c : ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] :
ContravariantClass αᵒᵈ αᵒᵈ (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
Equations
instance OrderDual.covariantClass_swap_add_lt {α : Type u} [inst : LT α] [inst : Add α] [c : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
CovariantClass αᵒᵈ αᵒᵈ (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
def OrderDual.covariantClass_swap_add_lt.proof_1 {α : Type u_1} [inst : LT α] [inst : Add α] [c : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
CovariantClass αᵒᵈ αᵒᵈ (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
Equations
instance OrderDual.covariantClass_swap_mul_lt {α : Type u} [inst : LT α] [inst : Mul α] [c : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] :
CovariantClass αᵒᵈ αᵒᵈ (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
Equations
def OrderDual.orderedAddCommMonoid.proof_2 {α : Type u_1} [inst : ] (a : αᵒᵈ) (b : αᵒᵈ) :
a bb aa = b
Equations
def OrderDual.orderedAddCommMonoid.proof_3 {α : Type u_1} [inst : ] :
∀ (x x_1 : αᵒᵈ), x x_1∀ (c : αᵒᵈ), c + x c + x_1
Equations
def OrderDual.orderedAddCommMonoid.proof_1 {α : Type u_1} [inst : ] (a : αᵒᵈ) (b : αᵒᵈ) :
a + b = b + a
Equations
instance OrderDual.orderedAddCommMonoid {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance OrderDual.orderedCommMonoid {α : Type u} [inst : ] :
Equations
instance OrderDual.orderedAddCancelCommMonoid {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
def OrderDual.orderedAddCancelCommMonoid.proof_1 {α : Type u_1} [inst : ] (a : αᵒᵈ) (b : αᵒᵈ) :
a b∀ (c : αᵒᵈ), c + a c + b
Equations
def OrderDual.orderedAddCancelCommMonoid.proof_2 {α : Type u_1} [inst : ] :
∀ (x x_1 x_2 : α), x + x_1 x + x_2x_1 x_2
Equations
instance OrderDual.orderedCancelCommMonoid {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance OrderDual.linearOrderedAddCancelCommMonoid {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
def OrderDual.linearOrderedAddCancelCommMonoid.proof_2 {α : Type u_1} [inst : ] (a : αᵒᵈ) (b : αᵒᵈ) (c : αᵒᵈ) :
a + b a + cb c
Equations
def OrderDual.linearOrderedAddCancelCommMonoid.proof_4 {α : Type u_1} [inst : ] (a : αᵒᵈ) (b : αᵒᵈ) :
min a b = if a b then a else b
Equations
def OrderDual.linearOrderedAddCancelCommMonoid.proof_5 {α : Type u_1} [inst : ] (a : αᵒᵈ) (b : αᵒᵈ) :
max a b = if a b then b else a
Equations
def OrderDual.linearOrderedAddCancelCommMonoid.proof_3 {α : Type u_1} [inst : ] (a : αᵒᵈ) (b : αᵒᵈ) :
a b b a
Equations
def OrderDual.linearOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} [inst : ] (a : αᵒᵈ) (b : αᵒᵈ) :
a b∀ (c : αᵒᵈ), c + a c + b
Equations
instance OrderDual.linearOrderedCancelCommMonoid {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
def OrderDual.linearOrderedAddCommMonoid.proof_3 {α : Type u_1} [inst : ] (a : αᵒᵈ) (b : αᵒᵈ) :
max a b = if a b then b else a
Equations
instance OrderDual.linearOrderedAddCommMonoid {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
def OrderDual.linearOrderedAddCommMonoid.proof_2 {α : Type u_1} [inst : ] (a : αᵒᵈ) (b : αᵒᵈ) :
min a b = if a b then a else b
Equations
def OrderDual.linearOrderedAddCommMonoid.proof_1 {α : Type u_1} [inst : ] (a : αᵒᵈ) (b : αᵒᵈ) :
a b b a
Equations
def OrderDual.linearOrderedAddCommMonoid.proof_4 {α : Type u_1} [inst : ] (a : αᵒᵈ) (b : αᵒᵈ) :
a b∀ (c : αᵒᵈ), c + a c + b
Equations
instance OrderDual.linearOrderedCommMonoid {α : Type u} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.