Ordered monoid structures on the order dual.

ink

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

Equations

• (_ : 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)

ink

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

Equations

• @OrderDual.contravariantClass_add_le = @OrderDual.contravariantClass_add_le.proof_1

ink

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

Equations

• @OrderDual.contravariantClass_mul_le = @OrderDual.contravariantClass_mul_le.proof_1

ink

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

Equations

• @OrderDual.covariantClass_add_le = @OrderDual.covariantClass_add_le.proof_1

ink

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

Equations

• (_ : 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)

ink

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

Equations

• @OrderDual.covariantClass_mul_le = @OrderDual.covariantClass_mul_le.proof_1

ink

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

Equations

• @OrderDual.contravariantClass_swap_add_le = @OrderDual.contravariantClass_swap_add_le.proof_1

ink

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)

ink

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

Equations

• @OrderDual.contravariantClass_swap_mul_le = @OrderDual.contravariantClass_swap_mul_le.proof_1

ink

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

Equations

• @OrderDual.covariantClass_swap_add_le = @OrderDual.covariantClass_swap_add_le.proof_1

ink

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)

ink

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

Equations

• @OrderDual.covariantClass_swap_mul_le = @OrderDual.covariantClass_swap_mul_le.proof_1

ink

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

Equations

• @OrderDual.contravariantClass_add_lt = @OrderDual.contravariantClass_add_lt.proof_1

ink

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

Equations

• (_ : 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)

ink

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

Equations

• @OrderDual.contravariantClass_mul_lt = @OrderDual.contravariantClass_mul_lt.proof_1

ink

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

Equations

• @OrderDual.covariantClass_add_lt = @OrderDual.covariantClass_add_lt.proof_1

ink

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

Equations

• (_ : 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)

ink

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

Equations

• @OrderDual.covariantClass_mul_lt = @OrderDual.covariantClass_mul_lt.proof_1

ink

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

Equations

• @OrderDual.contravariantClass_swap_add_lt = @OrderDual.contravariantClass_swap_add_lt.proof_1

ink

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)

ink

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

Equations

• @OrderDual.contravariantClass_swap_mul_lt = @OrderDual.contravariantClass_swap_mul_lt.proof_1

ink

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

Equations

• @OrderDual.covariantClass_swap_add_lt = @OrderDual.covariantClass_swap_add_lt.proof_1

ink

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)

ink

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

• @OrderDual.covariantClass_swap_mul_lt = @OrderDual.covariantClass_swap_mul_lt.proof_1

ink

def OrderDual.orderedAddCommMonoid.proof_2 {α : Type u_1} [inst : OrderedAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) : a ≤ b → b ≤ a → a = b

Equations

• (_ : ∀ (a b : αᵒᵈ), a ≤ b → b ≤ a → a = b) = (_ : ∀ (a b : αᵒᵈ), a ≤ b → b ≤ a → a = b)

ink

def OrderDual.orderedAddCommMonoid.proof_3 {α : Type u_1} [inst : OrderedAddCommMonoid α] : ∀ (x x_1 : αᵒᵈ), x ≤ x_1 → ∀ (c : αᵒᵈ), c + x ≤ c + x_1

Equations

• (_ : c + x ≤ c + x) = (_ : c + x ≤ c + x)

ink

def OrderDual.orderedAddCommMonoid.proof_1 {α : Type u_1} [inst : OrderedAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) : a + b = b + a

Equations

• (_ : ∀ (a b : αᵒᵈ), a + b = b + a) = (_ : ∀ (a b : αᵒᵈ), a + b = b + a)

ink

instance OrderDual.orderedAddCommMonoid {α : Type u} [inst : OrderedAddCommMonoid α] : OrderedAddCommMonoid αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

ink

instance OrderDual.orderedCommMonoid {α : Type u} [inst : OrderedCommMonoid α] : OrderedCommMonoid αᵒᵈ

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)

ink

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)

ink

instance OrderDual.OrderedCancelAddCommMonoid.to_contravariantClass {α : Type u} [inst : OrderedCancelAddCommMonoid α] : ContravariantClass αᵒᵈ αᵒᵈ Add.add LE.le

Equations

• @OrderDual.OrderedCancelAddCommMonoid.to_contravariantClass = @OrderDual.OrderedCancelAddCommMonoid.to_contravariantClass.proof_1

ink

instance OrderDual.OrderedCancelCommMonoid.to_contravariantClass {α : Type u} [inst : OrderedCancelCommMonoid α] : ContravariantClass αᵒᵈ αᵒᵈ Mul.mul LE.le

Equations

• @OrderDual.OrderedCancelCommMonoid.to_contravariantClass = @OrderDual.OrderedCancelCommMonoid.to_contravariantClass.proof_1

ink

instance OrderDual.orderedAddCancelCommMonoid {α : Type u} [inst : OrderedCancelAddCommMonoid α] : OrderedCancelAddCommMonoid αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

ink

def OrderDual.orderedAddCancelCommMonoid.proof_1 {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) : a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b

Equations

• (_ : ∀ (a b : αᵒᵈ), a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b) = (_ : ∀ (a b : αᵒᵈ), a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b)

ink

def OrderDual.orderedAddCancelCommMonoid.proof_2 {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] : ∀ (x x_1 x_2 : α), x + x_1 ≤ x + x_2 → x_1 ≤ x_2

Equations

• (_ : x + x ≤ x + x → x ≤ x) = (_ : x + x ≤ x + x → x ≤ x)

ink

instance OrderDual.orderedCancelCommMonoid {α : Type u} [inst : OrderedCancelCommMonoid α] : OrderedCancelCommMonoid αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

ink

instance OrderDual.linearOrderedAddCancelCommMonoid {α : Type u} [inst : LinearOrderedCancelAddCommMonoid α] : LinearOrderedCancelAddCommMonoid αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

ink

def OrderDual.linearOrderedAddCancelCommMonoid.proof_2 {α : Type u_1} [inst : LinearOrderedCancelAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) (c : αᵒᵈ) : a + b ≤ a + c → b ≤ c

Equations

• (_ : ∀ (a b c : αᵒᵈ), a + b ≤ a + c → b ≤ c) = (_ : ∀ (a b c : αᵒᵈ), a + b ≤ a + c → b ≤ c)

ink

def OrderDual.linearOrderedAddCancelCommMonoid.proof_4 {α : Type u_1} [inst : LinearOrderedCancelAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) : min a b = if a ≤ b then a else b

Equations

• (_ : ∀ (a b : αᵒᵈ), min a b = if a ≤ b then a else b) = (_ : ∀ (a b : αᵒᵈ), min a b = if a ≤ b then a else b)

ink

def OrderDual.linearOrderedAddCancelCommMonoid.proof_5 {α : Type u_1} [inst : LinearOrderedCancelAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) : max a b = if a ≤ b then b else a

Equations

• (_ : ∀ (a b : αᵒᵈ), max a b = if a ≤ b then b else a) = (_ : ∀ (a b : αᵒᵈ), max a b = if a ≤ b then b else a)

ink

def OrderDual.linearOrderedAddCancelCommMonoid.proof_3 {α : Type u_1} [inst : LinearOrderedCancelAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) : a ≤ b ∨ b ≤ a

Equations

• (_ : ∀ (a b : αᵒᵈ), a ≤ b ∨ b ≤ a) = (_ : ∀ (a b : αᵒᵈ), a ≤ b ∨ b ≤ a)

ink

def OrderDual.linearOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} [inst : LinearOrderedCancelAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) : a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b

Equations

• (_ : ∀ (a b : αᵒᵈ), a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b) = (_ : ∀ (a b : αᵒᵈ), a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b)

ink

instance OrderDual.linearOrderedCancelCommMonoid {α : Type u} [inst : LinearOrderedCancelCommMonoid α] : LinearOrderedCancelCommMonoid αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

ink

def OrderDual.linearOrderedAddCommMonoid.proof_3 {α : Type u_1} [inst : LinearOrderedAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) : max a b = if a ≤ b then b else a

Equations

• (_ : ∀ (a b : αᵒᵈ), max a b = if a ≤ b then b else a) = (_ : ∀ (a b : αᵒᵈ), max a b = if a ≤ b then b else a)

ink

instance OrderDual.linearOrderedAddCommMonoid {α : Type u} [inst : LinearOrderedAddCommMonoid α] : LinearOrderedAddCommMonoid αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

ink

def OrderDual.linearOrderedAddCommMonoid.proof_2 {α : Type u_1} [inst : LinearOrderedAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) : min a b = if a ≤ b then a else b

Equations

• (_ : ∀ (a b : αᵒᵈ), min a b = if a ≤ b then a else b) = (_ : ∀ (a b : αᵒᵈ), min a b = if a ≤ b then a else b)

ink

def OrderDual.linearOrderedAddCommMonoid.proof_1 {α : Type u_1} [inst : LinearOrderedAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) : a ≤ b ∨ b ≤ a

Equations

• (_ : ∀ (a b : αᵒᵈ), a ≤ b ∨ b ≤ a) = (_ : ∀ (a b : αᵒᵈ), a ≤ b ∨ b ≤ a)

ink

def OrderDual.linearOrderedAddCommMonoid.proof_4 {α : Type u_1} [inst : LinearOrderedAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) : a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b

Equations

• (_ : ∀ (a b : αᵒᵈ), a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b) = (_ : ∀ (a b : αᵒᵈ), a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b)

ink

instance OrderDual.linearOrderedCommMonoid {α : Type u} [inst : LinearOrderedCommMonoid α] : LinearOrderedCommMonoid αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.