Documentation

Mathlib.Algebra.Order.Monoid.OrderDual

Ordered monoid structures on the order dual. #

source
instance OrderDual.orderedAddCommMonoid {α : Type u} [OrderedAddCommMonoid α] :
OrderedAddCommMonoid αᵒᵈ
Equations
source
theorem OrderDual.orderedAddCommMonoid.proof_1 {α : Type u_1} [OrderedAddCommMonoid α] :
∀ (x x_1 : αᵒᵈ), x ≤ x_1 → ∀ (c : αᵒᵈ), c + x ≤ c + x_1
source
instance OrderDual.orderedCommMonoid {α : Type u} [OrderedCommMonoid α] :
OrderedCommMonoid αᵒᵈ
Equations
source
instance OrderDual.OrderedCancelAddCommMonoid.to_contravariantClass {α : Type u} [OrderedCancelAddCommMonoid α] :
ContravariantClass αᵒᵈ αᵒᵈ HAdd.hAdd LE.le
Equations
  • ⋯ = ⋯
source
instance OrderDual.OrderedCancelCommMonoid.to_contravariantClass {α : Type u} [OrderedCancelCommMonoid α] :
ContravariantClass αᵒᵈ αᵒᵈ HMul.hMul LE.le
Equations
  • ⋯ = ⋯
source
instance OrderDual.orderedAddCancelCommMonoid {α : Type u} [OrderedCancelAddCommMonoid α] :
OrderedCancelAddCommMonoid αᵒᵈ
Equations
source
theorem OrderDual.orderedAddCancelCommMonoid.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] :
∀ (x x_1 x_2 : α), x + x_1 ≤ x + x_2 → x_1 ≤ x_2
source
instance OrderDual.orderedCancelCommMonoid {α : Type u} [OrderedCancelCommMonoid α] :
OrderedCancelCommMonoid αᵒᵈ
Equations
source
theorem OrderDual.linearOrderedAddCancelCommMonoid.proof_2 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) (c : αᵒᵈ) :
a + b ≤ a + c → b ≤ c
source
theorem OrderDual.linearOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) :
a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b
source
theorem OrderDual.linearOrderedAddCancelCommMonoid.proof_4 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) :
min a b = if a ≤ b then a else b
source
theorem OrderDual.linearOrderedAddCancelCommMonoid.proof_6 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) :
compare a b = compareOfLessAndEq a b
source
instance OrderDual.linearOrderedAddCancelCommMonoid {α : Type u} [LinearOrderedCancelAddCommMonoid α] :
LinearOrderedCancelAddCommMonoid αᵒᵈ
Equations
  • One or more equations did not get rendered due to their size.
source
theorem OrderDual.linearOrderedAddCancelCommMonoid.proof_5 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) :
max a b = if a ≤ b then b else a
source
theorem OrderDual.linearOrderedAddCancelCommMonoid.proof_3 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) :
a ≤ b ∨ b ≤ a
source
instance OrderDual.linearOrderedCancelCommMonoid {α : Type u} [LinearOrderedCancelCommMonoid α] :
LinearOrderedCancelCommMonoid αᵒᵈ
Equations
  • One or more equations did not get rendered due to their size.
source
theorem OrderDual.linearOrderedAddCommMonoid.proof_5 {α : Type u_1} [LinearOrderedAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) :
compare a b = compareOfLessAndEq a b
source
theorem OrderDual.linearOrderedAddCommMonoid.proof_3 {α : Type u_1} [LinearOrderedAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) :
min a b = if a ≤ b then a else b
source
instance OrderDual.linearOrderedAddCommMonoid {α : Type u} [LinearOrderedAddCommMonoid α] :
LinearOrderedAddCommMonoid αᵒᵈ
Equations
  • One or more equations did not get rendered due to their size.
source
theorem OrderDual.linearOrderedAddCommMonoid.proof_4 {α : Type u_1} [LinearOrderedAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) :
max a b = if a ≤ b then b else a
source
theorem OrderDual.linearOrderedAddCommMonoid.proof_2 {α : Type u_1} [LinearOrderedAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) :
a ≤ b ∨ b ≤ a
source
theorem OrderDual.linearOrderedAddCommMonoid.proof_1 {α : Type u_1} [LinearOrderedAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) :
a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b
source
instance OrderDual.linearOrderedCommMonoid {α : Type u} [LinearOrderedCommMonoid α] :
LinearOrderedCommMonoid αᵒᵈ
Equations
  • One or more equations did not get rendered due to their size.