Documentation

Mathlib.Algebra.Order.Monoid.Prod

Products of ordered monoids #

theorem Prod.instOrderedAddCommMonoid.proof_1 {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] :
∀ (x x_1 : α × β), x x_1∀ (x_2 : α × β), (x_2 + x).1 (x_2 + x_1).1 (x_2 + x).2 (x_2 + x_1).2
Equations
Equations
Equations
theorem Prod.instOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} {β : Type u_2} [OrderedCancelAddCommMonoid α] [OrderedCancelAddCommMonoid β] :
∀ (x x_1 x_2 : α × β), x + x_1 x + x_2x_1.1 x_2.1 x_1.2 x_2.2
Equations
instance Prod.instExistsAddOfLE {α : Type u_1} {β : Type u_2} [LE α] [LE β] [Add α] [Add β] [ExistsAddOfLE α] [ExistsAddOfLE β] :
Equations
  • =
instance Prod.instExistsMulOfLE {α : Type u_1} {β : Type u_2} [LE α] [LE β] [Mul α] [Mul β] [ExistsMulOfLE α] [ExistsMulOfLE β] :
Equations
  • =
theorem Prod.instCanonicallyOrderedAddCommMonoid.proof_2 {α : Type u_1} {β : Type u_2} [CanonicallyOrderedAddCommMonoid α] [CanonicallyOrderedAddCommMonoid β] :
∀ {a b : α × β}, a b∃ (c : α × β), b = a + c
instance Prod.Lex.orderedAddCommMonoid {α : Type u_1} {β : Type u_2} [OrderedAddCommMonoid α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [OrderedAddCommMonoid β] :
Equations
theorem Prod.Lex.orderedAddCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} [OrderedAddCommMonoid α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [OrderedAddCommMonoid β] :
∀ (x x_1 : Lex (α × β)), x x_1∀ (z : Lex (α × β)), z + x z + x_1
instance Prod.Lex.orderedCommMonoid {α : Type u_1} {β : Type u_2} [OrderedCommMonoid α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [OrderedCommMonoid β] :
Equations
theorem Prod.Lex.orderedAddCancelCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} [OrderedCancelAddCommMonoid α] [OrderedCancelAddCommMonoid β] :
∀ (x x_1 : Lex (α × β)), x x_1∀ (a : Lex (α × β)), a + x a + x_1
Equations
theorem Prod.Lex.orderedAddCancelCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} [OrderedCancelAddCommMonoid α] [OrderedCancelAddCommMonoid β] :
∀ (x x_1 x_2 : Lex (α × β)), x + x_1 x + x_2x_1 x_2
Equations
theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_4 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) :
min a b = if a b then a else b
Equations
theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_1 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) :
a b∀ (c : Lex (α × β)), c + a c + b
theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_2 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) (c : Lex (α × β)) :
a + b a + cb c
theorem Prod.Lex.linearOrderedAddCancelCommMonoid.proof_5 {α : Type u_2} {β : Type u_1} [LinearOrderedCancelAddCommMonoid α] [LinearOrderedCancelAddCommMonoid β] (a : Lex (α × β)) (b : Lex (α × β)) :
max a b = if a b then b else a
Equations