Documentation

Mathlib.Algebra.Order.Group.PiLex

Lexicographic product of algebraic order structures #

This file proves that the lexicographic order on pi types is compatible with the pointwise algebraic operations.

theorem Pi.Lex.orderedAddCancelCommMonoid.proof_1 {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [(i : ι) → OrderedCancelAddCommMonoid (α i)] :
∀ (x x_1 : Lex ((i : ι) → α i)), x x_1∀ (z : Lex ((i : ι) → α i)), z + x z + x_1
theorem Pi.Lex.orderedAddCancelCommMonoid.proof_2 {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [(i : ι) → OrderedCancelAddCommMonoid (α i)] :
∀ (x x_1 x_2 : Lex ((i : ι) → α i)), x + x_1 x + x_2x_1 x_2
instance Pi.Lex.orderedAddCancelCommMonoid {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [(i : ι) → OrderedCancelAddCommMonoid (α i)] :
OrderedCancelAddCommMonoid (Lex ((i : ι) → α i))
Equations
instance Pi.Lex.orderedCancelCommMonoid {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [(i : ι) → OrderedCancelCommMonoid (α i)] :
OrderedCancelCommMonoid (Lex ((i : ι) → α i))
Equations
theorem Pi.Lex.orderedAddCommGroup.proof_1 {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [(i : ι) → OrderedAddCommGroup (α i)] :
∀ (x x_1 : Lex ((i : ι) → α i)), x x_1∀ (a : Lex ((i : ι) → α i)), a + x a + x_1
instance Pi.Lex.orderedAddCommGroup {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [(i : ι) → OrderedAddCommGroup (α i)] :
OrderedAddCommGroup (Lex ((i : ι) → α i))
Equations
instance Pi.Lex.orderedCommGroup {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [(i : ι) → OrderedCommGroup (α i)] :
OrderedCommGroup (Lex ((i : ι) → α i))
Equations
theorem Pi.Lex.linearOrderedAddCancelCommMonoid.proof_4 {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [(i : ι) → LinearOrderedCancelAddCommMonoid (α i)] (a : Lex ((i : ι) → α i)) (b : Lex ((i : ι) → α i)) :
min a b = if a b then a else b
theorem Pi.Lex.linearOrderedAddCancelCommMonoid.proof_6 {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [(i : ι) → LinearOrderedCancelAddCommMonoid (α i)] (a : Lex ((i : ι) → α i)) (b : Lex ((i : ι) → α i)) :
noncomputable instance Pi.Lex.linearOrderedAddCancelCommMonoid {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [(i : ι) → LinearOrderedCancelAddCommMonoid (α i)] :
Equations
theorem Pi.Lex.linearOrderedAddCancelCommMonoid.proof_1 {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [(i : ι) → LinearOrderedCancelAddCommMonoid (α i)] (a : Lex ((i : ι) → α i)) (b : Lex ((i : ι) → α i)) :
a b∀ (c : Lex ((i : ι) → α i)), c + a c + b
theorem Pi.Lex.linearOrderedAddCancelCommMonoid.proof_5 {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [(i : ι) → LinearOrderedCancelAddCommMonoid (α i)] (a : Lex ((i : ι) → α i)) (b : Lex ((i : ι) → α i)) :
max a b = if a b then b else a
theorem Pi.Lex.linearOrderedAddCancelCommMonoid.proof_2 {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [(i : ι) → LinearOrderedCancelAddCommMonoid (α i)] (a : Lex ((i : ι) → α i)) (b : Lex ((i : ι) → α i)) (c : Lex ((i : ι) → α i)) :
a + b a + cb c
theorem Pi.Lex.linearOrderedAddCancelCommMonoid.proof_3 {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [(i : ι) → LinearOrderedCancelAddCommMonoid (α i)] (a : Lex ((i : ι) → α i)) (b : Lex ((i : ι) → α i)) :
a b b a
noncomputable instance Pi.Lex.linearOrderedCancelCommMonoid {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [(i : ι) → LinearOrderedCancelCommMonoid (α i)] :
LinearOrderedCancelCommMonoid (Lex ((i : ι) → α i))
Equations
noncomputable instance Pi.Lex.linearOrderedAddCommGroup {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [(i : ι) → LinearOrderedAddCommGroup (α i)] :
LinearOrderedAddCommGroup (Lex ((i : ι) → α i))
Equations
  • Pi.Lex.linearOrderedAddCommGroup = LinearOrderedAddCommGroup.mk LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT
theorem Pi.Lex.linearOrderedAddCommGroup.proof_3 {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [(i : ι) → LinearOrderedAddCommGroup (α i)] (a : Lex ((i : ι) → α i)) (b : Lex ((i : ι) → α i)) :
min a b = if a b then a else b
theorem Pi.Lex.linearOrderedAddCommGroup.proof_1 {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [(i : ι) → LinearOrderedAddCommGroup (α i)] :
∀ (x x_1 : Lex ((i : ι) → α i)), x x_1∀ (a : Lex ((i : ι) → α i)), a + x a + x_1
theorem Pi.Lex.linearOrderedAddCommGroup.proof_5 {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [(i : ι) → LinearOrderedAddCommGroup (α i)] (a : Lex ((i : ι) → α i)) (b : Lex ((i : ι) → α i)) :
theorem Pi.Lex.linearOrderedAddCommGroup.proof_2 {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [(i : ι) → LinearOrderedAddCommGroup (α i)] (a : Lex ((i : ι) → α i)) (b : Lex ((i : ι) → α i)) :
a b b a
theorem Pi.Lex.linearOrderedAddCommGroup.proof_4 {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [(i : ι) → LinearOrderedAddCommGroup (α i)] (a : Lex ((i : ι) → α i)) (b : Lex ((i : ι) → α i)) :
max a b = if a b then b else a
noncomputable instance Pi.Lex.linearOrderedCommGroup {ι : Type u_1} {α : ιType u_2} [LinearOrder ι] [IsWellOrder ι fun (x1 x2 : ι) => x1 < x2] [(i : ι) → LinearOrderedCommGroup (α i)] :
LinearOrderedCommGroup (Lex ((i : ι) → α i))
Equations
  • Pi.Lex.linearOrderedCommGroup = LinearOrderedCommGroup.mk LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT