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_2 → x_1 ≤ x_2

instance Pi.Lex.orderedAddCancelCommMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → OrderedCancelAddCommMonoid (α i)] : OrderedCancelAddCommMonoid (Lex ((i : ι) → α i))

Equations

• Pi.Lex.orderedAddCancelCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

abbrev Pi.Lex.orderedAddCancelCommMonoid.match_1 {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → OrderedCancelAddCommMonoid (α i)] : ∀ (x x_1 : Lex ((i : ι) → α i)) (motive : x < x_1 → Prop) (x_2 : x < x_1), (∀ (i : ι) (hi : (∀ j < i, x j = x_1 j) ∧ (fun (x : ι) (x_3 x_4 : α x) => x_3 < x_4) i (x i) (x_1 i)), motive ⋯) → motive x_2

Equations

• ⋯ = ⋯

abbrev Pi.Lex.orderedAddCancelCommMonoid.match_2 {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → OrderedCancelAddCommMonoid (α i)] : ∀ (x x_1 x_2 : Lex ((i : ι) → α i)) (motive : x + x_1 < x + x_2 → Prop) (x_3 : x + x_1 < x + x_2), (∀ (i : ι) (hi : (∀ j < i, (x + x_1) j = (x + x_2) j) ∧ (fun (x : ι) (x_4 x_5 : α x) => x_4 < x_5) i ((x + x_1) i) ((x + x_2) i)), motive ⋯) → motive x_3

Equations

• ⋯ = ⋯

instance Pi.Lex.orderedCancelCommMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → OrderedCancelCommMonoid (α i)] : OrderedCancelCommMonoid (Lex ((i : ι) → α i))

Equations

• Pi.Lex.orderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯

instance Pi.Lex.orderedAddCommGroup {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → OrderedAddCommGroup (α i)] : OrderedAddCommGroup (Lex ((i : ι) → α i))

Equations

• Pi.Lex.orderedAddCommGroup = OrderedAddCommGroup.mk ⋯

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.orderedCommGroup {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [(i : ι) → OrderedCommGroup (α i)] : OrderedCommGroup (Lex ((i : ι) → α i))

Equations

• Pi.Lex.orderedCommGroup = OrderedCommGroup.mk ⋯

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

noncomputable instance Pi.Lex.linearOrderedAddCancelCommMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → LinearOrderedCancelAddCommMonoid (α i)] : LinearOrderedCancelAddCommMonoid (Lex ((i : ι) → α i))

Equations

• One or more equations did not get rendered due to their size.

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 + c → b ≤ c

theorem Pi.Lex.linearOrderedAddCancelCommMonoid.proof_5 {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(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_6 {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → LinearOrderedCancelAddCommMonoid (α i)] (a : Lex ((i : ι) → α i)) (b : Lex ((i : ι) → α i)) : compare a b = compareOfLessAndEq a b

theorem Pi.Lex.linearOrderedAddCancelCommMonoid.proof_3 {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → LinearOrderedCancelAddCommMonoid (α i)] (a : Lex ((i : ι) → α i)) (b : Lex ((i : ι) → α i)) : a ≤ b ∨ b ≤ a

theorem Pi.Lex.linearOrderedAddCancelCommMonoid.proof_4 {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → LinearOrderedCancelAddCommMonoid (α i)] (a : Lex ((i : ι) → α i)) (b : Lex ((i : ι) → α i)) : min a b = if a ≤ b then a else b

noncomputable instance Pi.Lex.linearOrderedCancelCommMonoid {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → LinearOrderedCancelCommMonoid (α i)] : LinearOrderedCancelCommMonoid (Lex ((i : ι) → α i))

Equations

• One or more equations did not get rendered due to their size.

theorem Pi.Lex.linearOrderedAddCommGroup.proof_4 {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → LinearOrderedAddCommGroup (α i)] (a : Lex ((i : ι) → α i)) (b : Lex ((i : ι) → α i)) : max a b = if a ≤ b then b else a

theorem Pi.Lex.linearOrderedAddCommGroup.proof_5 {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → LinearOrderedAddCommGroup (α i)] (a : Lex ((i : ι) → α i)) (b : Lex ((i : ι) → α i)) : compare a b = compareOfLessAndEq a b

theorem Pi.Lex.linearOrderedAddCommGroup.proof_1 {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → LinearOrderedAddCommGroup (α i)] : ∀ (x x_1 : Lex ((i : ι) → α i)), x ≤ x_1 → ∀ (a : Lex ((i : ι) → α i)), a + x ≤ a + x_1

noncomputable instance Pi.Lex.linearOrderedAddCommGroup {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → LinearOrderedAddCommGroup (α i)] : LinearOrderedAddCommGroup (Lex ((i : ι) → α i))

Equations

• Pi.Lex.linearOrderedAddCommGroup = let __spread.0 := inferInstance; LinearOrderedAddCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

theorem Pi.Lex.linearOrderedAddCommGroup.proof_2 {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → LinearOrderedAddCommGroup (α i)] (a : Lex ((i : ι) → α i)) (b : Lex ((i : ι) → α i)) : a ≤ b ∨ b ≤ a

theorem Pi.Lex.linearOrderedAddCommGroup.proof_3 {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → LinearOrderedAddCommGroup (α i)] (a : Lex ((i : ι) → α i)) (b : Lex ((i : ι) → α i)) : min a b = if a ≤ b then a else b

noncomputable instance Pi.Lex.linearOrderedCommGroup {ι : Type u_1} {α : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → LinearOrderedCommGroup (α i)] : LinearOrderedCommGroup (Lex ((i : ι) → α i))

Equations

• Pi.Lex.linearOrderedCommGroup = let __spread.0 := inferInstance; LinearOrderedCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯