Ordered monoid structures on the order dual. #
Equations
- OrderDual.orderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯
Equations
- OrderDual.orderedCommMonoid = OrderedCommMonoid.mk ⋯
instance
OrderDual.OrderedCancelAddCommMonoid.to_contravariantClass
{α : Type u}
[OrderedCancelAddCommMonoid α]
:
ContravariantClass αᵒᵈ αᵒᵈ HAdd.hAdd LE.le
Equations
- ⋯ = ⋯
instance
OrderDual.OrderedCancelCommMonoid.to_contravariantClass
{α : Type u}
[OrderedCancelCommMonoid α]
:
ContravariantClass αᵒᵈ αᵒᵈ HMul.hMul LE.le
Equations
- ⋯ = ⋯
Equations
- OrderDual.orderedAddCancelCommMonoid = OrderedCancelAddCommMonoid.mk ⋯
theorem
OrderDual.orderedAddCancelCommMonoid.proof_1
{α : Type u_1}
[OrderedCancelAddCommMonoid α]
:
Equations
- OrderDual.orderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯
theorem
OrderDual.linearOrderedAddCancelCommMonoid.proof_4
{α : Type u_1}
[LinearOrderedCancelAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
theorem
OrderDual.linearOrderedAddCancelCommMonoid.proof_6
{α : Type u_1}
[LinearOrderedCancelAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
compare a b = compareOfLessAndEq a b
instance
OrderDual.linearOrderedAddCancelCommMonoid
{α : Type u}
[LinearOrderedCancelAddCommMonoid α]
:
Equations
- One or more equations did not get rendered due to their size.
theorem
OrderDual.linearOrderedAddCancelCommMonoid.proof_5
{α : Type u_1}
[LinearOrderedCancelAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
theorem
OrderDual.linearOrderedAddCancelCommMonoid.proof_3
{α : Type u_1}
[LinearOrderedCancelAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
Equations
- One or more equations did not get rendered due to their size.
theorem
OrderDual.linearOrderedAddCommMonoid.proof_5
{α : Type u_1}
[LinearOrderedAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
compare a b = compareOfLessAndEq a b
theorem
OrderDual.linearOrderedAddCommMonoid.proof_3
{α : Type u_1}
[LinearOrderedAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
Equations
- One or more equations did not get rendered due to their size.
theorem
OrderDual.linearOrderedAddCommMonoid.proof_4
{α : Type u_1}
[LinearOrderedAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
theorem
OrderDual.linearOrderedAddCommMonoid.proof_2
{α : Type u_1}
[LinearOrderedAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
Equations
- One or more equations did not get rendered due to their size.