Documentation

Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual

Unbundled ordered monoid structures on the order dual. #

instance OrderDual.contravariantClass_add_le {α : Type u} [LE α] [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} [LE α] [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} [LE α] [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} [LE α] [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} [LE α] [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} [LE α] [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} [LE α] [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} [LE α] [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} [LT α] [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} [LT α] [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} [LT α] [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} [LT α] [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} [LT α] [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} [LT α] [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} [LT α] [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} [LT α] [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
  • =