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
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
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
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
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
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
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
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
- (_ : 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}
[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
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
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
- (_ : 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}
[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
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
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
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
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
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
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
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
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
- (_ : 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}
[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
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
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
- (_ : 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}
[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
- One or more equations did not get rendered due to their size.
Equations
- OrderDual.orderedCommMonoid = let src := OrderDual.partialOrder α; let src_1 := instCommMonoidOrderDual; OrderedCommMonoid.mk (_ : ∀ (x x_1 : αᵒᵈ), x ≤ x_1 → ∀ (c : αᵒᵈ), c * x ≤ c * x_1)
def
OrderDual.OrderedCancelAddCommMonoid.to_contravariantClass.proof_1
{α : Type u_1}
[inst : OrderedCancelAddCommMonoid α]
:
ContravariantClass αᵒᵈ αᵒᵈ Add.add LE.le
Equations
- (_ : ContravariantClass αᵒᵈ αᵒᵈ Add.add LE.le) = (_ : ContravariantClass αᵒᵈ αᵒᵈ Add.add LE.le)
instance
OrderDual.OrderedCancelAddCommMonoid.to_contravariantClass
{α : Type u}
[inst : OrderedCancelAddCommMonoid α]
:
ContravariantClass αᵒᵈ αᵒᵈ Add.add LE.le
instance
OrderDual.OrderedCancelCommMonoid.to_contravariantClass
{α : Type u}
[inst : OrderedCancelCommMonoid α]
:
ContravariantClass αᵒᵈ αᵒᵈ Mul.mul LE.le
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
instance
OrderDual.linearOrderedAddCancelCommMonoid
{α : Type u}
[inst : LinearOrderedCancelAddCommMonoid α]
:
Equations
- One or more equations did not get rendered due to their size.
def
OrderDual.linearOrderedAddCancelCommMonoid.proof_1
{α : Type u_1}
[inst : LinearOrderedCancelAddCommMonoid α]
(a : αᵒᵈ)
(b : αᵒᵈ)
:
instance
OrderDual.linearOrderedCancelCommMonoid
{α : Type u}
[inst : LinearOrderedCancelCommMonoid α]
:
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.