Documentation

Mathlib.Algebra.Order.Group.Prod

Products of ordered commutative groups. #

theorem Prod.instOrderedAddCommGroup.proof_1 {G : Type u_1} {H : Type u_2} [OrderedAddCommGroup G] [OrderedAddCommGroup H] (a : G × H) (b : G × H) :
a b∀ (c : G × H), c + a c + b
Equations
Equations
theorem Prod.Lex.orderedAddCommGroup.proof_1 {G : Type u_2} {H : Type u_1} [OrderedAddCommGroup G] [OrderedAddCommGroup H] :
∀ (x x_1 : Lex (G × H)), x x_1∀ (a : Lex (G × H)), a + x a + x_1
Equations
Equations
theorem Prod.Lex.linearOrderedAddCommGroup.proof_3 {G : Type u_2} {H : Type u_1} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup H] (a : Lex (G × H)) (b : Lex (G × H)) :
min a b = if a b then a else b
Equations
  • Prod.Lex.linearOrderedAddCommGroup = let __spread.0 := inferInstance; LinearOrderedAddCommGroup.mk LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT
theorem Prod.Lex.linearOrderedAddCommGroup.proof_4 {G : Type u_2} {H : Type u_1} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup H] (a : Lex (G × H)) (b : Lex (G × H)) :
max a b = if a b then b else a
theorem Prod.Lex.linearOrderedAddCommGroup.proof_1 {G : Type u_2} {H : Type u_1} [LinearOrderedAddCommGroup G] [LinearOrderedAddCommGroup H] :
∀ (x x_1 : Lex (G × H)), x x_1∀ (a : Lex (G × H)), a + x a + x_1
Equations
  • Prod.Lex.linearOrderedCommGroup = let __spread.0 := inferInstance; LinearOrderedCommGroup.mk LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT