Ordered monoid structures on the order dual. #
theorem
OrderDual.contravariantClass_add_le.proof_1
{α : Type u_1}
[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
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
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
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
theorem
OrderDual.covariantClass_add_le.proof_1
{α : Type u_1}
[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
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
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
theorem
OrderDual.contravariantClass_swap_add_le.proof_1
{α : Type u_1}
[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
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
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
theorem
OrderDual.covariantClass_swap_add_le.proof_1
{α : Type u_1}
[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
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
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
theorem
OrderDual.contravariantClass_add_lt.proof_1
{α : Type u_1}
[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
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
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
theorem
OrderDual.covariantClass_add_lt.proof_1
{α : Type u_1}
[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
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
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
theorem
OrderDual.contravariantClass_swap_add_lt.proof_1
{α : Type u_1}
[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
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
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
theorem
OrderDual.covariantClass_swap_add_lt.proof_1
{α : Type u_1}
[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
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
theorem
OrderDual.orderedAddCommMonoid.proof_2
{α : Type u_1}
[OrderedAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
theorem
OrderDual.orderedAddCommMonoid.proof_1
{α : Type u_1}
[OrderedAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
theorem
OrderDual.OrderedCancelAddCommMonoid.to_contravariantClass.proof_1
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
:
ContravariantClass αᵒᵈ αᵒᵈ Add.add LE.le
instance
OrderDual.OrderedCancelAddCommMonoid.to_contravariantClass
{α : Type u}
[OrderedCancelAddCommMonoid α]
:
ContravariantClass αᵒᵈ αᵒᵈ Add.add LE.le
instance
OrderDual.OrderedCancelCommMonoid.to_contravariantClass
{α : Type u}
[OrderedCancelCommMonoid α]
:
ContravariantClass αᵒᵈ αᵒᵈ Mul.mul LE.le
theorem
OrderDual.orderedAddCancelCommMonoid.proof_2
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
:
theorem
OrderDual.linearOrderedAddCancelCommMonoid.proof_5
{α : Type u_1}
[LinearOrderedCancelAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
theorem
OrderDual.linearOrderedAddCancelCommMonoid.proof_6
{α : Type u_1}
[LinearOrderedCancelAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
compare a b = compareOfLessAndEq a b
theorem
OrderDual.linearOrderedAddCancelCommMonoid.proof_3
{α : Type u_1}
[LinearOrderedCancelAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
theorem
OrderDual.linearOrderedAddCancelCommMonoid.proof_4
{α : Type u_1}
[LinearOrderedCancelAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
theorem
OrderDual.linearOrderedAddCommMonoid.proof_2
{α : Type u_1}
[LinearOrderedAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
theorem
OrderDual.linearOrderedAddCommMonoid.proof_1
{α : Type u_1}
[LinearOrderedAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
theorem
OrderDual.linearOrderedAddCommMonoid.proof_4
{α : Type u_1}
[LinearOrderedAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
compare a b = compareOfLessAndEq a b
theorem
OrderDual.linearOrderedAddCommMonoid.proof_3
{α : Type u_1}
[LinearOrderedAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
: