Unbundled ordered monoid structures on the order dual. #
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_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
- ⋯ = ⋯