Ordered monoid structures on the order dual.

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

Equations

• OrderDual.orderedCommMonoid = OrderedCommMonoid.mk ⋯

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

Equations

• OrderDual.orderedAddCommMonoid = OrderedAddCommMonoid.mk ⋯

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

instance OrderDual.OrderedCancelCommMonoid.to_contravariantClass {α : Type u} [OrderedCancelCommMonoid α] : ContravariantClass αᵒᵈ αᵒᵈ HMul.hMul LE.le

Equations

• ⋯ = ⋯

instance OrderDual.OrderedCancelAddCommMonoid.to_contravariantClass {α : Type u} [OrderedCancelAddCommMonoid α] : ContravariantClass αᵒᵈ αᵒᵈ HAdd.hAdd LE.le

Equations

• ⋯ = ⋯

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

Equations

• OrderDual.orderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯

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

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

Equations

• OrderDual.orderedAddCancelCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

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

Equations

• OrderDual.linearOrderedCancelCommMonoid = LinearOrderedCancelCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

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

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

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

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

Equations

• OrderDual.linearOrderedAddCancelCommMonoid = LinearOrderedCancelAddCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

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

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

theorem OrderDual.linearOrderedAddCancelCommMonoid.proof_6 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) : compare a b = compareOfLessAndEq a b

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

Equations

• OrderDual.linearOrderedCommMonoid = LinearOrderedCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

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

theorem OrderDual.linearOrderedAddCommMonoid.proof_5 {α : Type u_1} [LinearOrderedAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) : compare a b = compareOfLessAndEq a b

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

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

Equations

• OrderDual.linearOrderedAddCommMonoid = LinearOrderedAddCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

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

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