Documentation

Mathlib.Algebra.Order.Monoid.OrderDual

Ordered monoid structures on the order dual. #

Equations
theorem OrderDual.orderedAddCommMonoid.proof_1 {α : Type u_1} [OrderedAddCommMonoid α] :
∀ (x x_1 : αᵒᵈ), x x_1∀ (c : αᵒᵈ), c + x c + x_1
Equations
theorem OrderDual.orderedAddCancelCommMonoid.proof_1 {α : Type u_1} [OrderedCancelAddCommMonoid α] :
∀ (x x_1 x_2 : α), x + x_1 x + x_2x_1 x_2
theorem OrderDual.linearOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} [LinearOrderedCancelAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) :
a b∀ (c : αᵒᵈ), c + a c + b
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.
theorem OrderDual.linearOrderedAddCommMonoid.proof_3 {α : Type u_1} [LinearOrderedAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) :
min a b = if a b then a else 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 : αᵒᵈ) :
max a b = if a b then b else a
theorem OrderDual.linearOrderedAddCommMonoid.proof_1 {α : Type u_1} [LinearOrderedAddCommMonoid α] (a : αᵒᵈ) (b : αᵒᵈ) :
a b∀ (c : αᵒᵈ), c + a c + b
Equations
  • One or more equations did not get rendered due to their size.