Lexicographic order on Pi types

This file defines the lexicographic order for Pi types. a is less than b if a i = b i for all i up to some point k, and a k < b k.

Notation

• Πₗ i, α i: Pi type equipped with the lexicographic order. Type synonym of Π i, α i.

See also

Related files are:

• Data.Finset.Colex: Colexicographic order on finite sets.
• Data.List.Lex: Lexicographic order on lists.
• Data.Sigma.Order: Lexicographic order on Σₗ i, α i.
• Data.PSigma.Order: Lexicographic order on Σₗ' i, α i.
• Data.Prod.Lex: Lexicographic order on α × β.

def Pi.Lex {ι : Type u_1} {β : ι → Type u_2} (r : ι → ι → Prop) (s : {i : ι} → β i → β i → Prop) (x : (i : ι) → β i) (y : (i : ι) → β i) : Prop

The lexicographic relation on Π i : ι, β i, where ι is ordered by r, and each β i is ordered by s.

Equations

• Pi.Lex r s x y = ∃ (i : ι), (∀ (j : ι), r j i → x j = y j) ∧ s (x i) (y i)

def Pi.«termΠₗ_,_» : Lean.ParserDescr

The notation Πₗ i, α i refers to a pi type equipped with the lexicographic order.

Equations

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

@[simp]

theorem Pi.toLex_apply {ι : Type u_1} {β : ι → Type u_2} (x : (i : ι) → β i) (i : ι) : toLex x i = x i

@[simp]

theorem Pi.ofLex_apply {ι : Type u_1} {β : ι → Type u_2} (x : Lex ((i : ι) → β i)) (i : ι) : ofLex x i = x i

theorem Pi.lex_lt_of_lt_of_preorder {ι : Type u_1} {β : ι → Type u_2} [(i : ι) → Preorder (β i)] {r : ι → ι → Prop} (hwf : WellFounded r) {x : (i : ι) → β i} {y : (i : ι) → β i} (hlt : x < y) : ∃ (i : ι), (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

theorem Pi.lex_lt_of_lt {ι : Type u_1} {β : ι → Type u_2} [(i : ι) → PartialOrder (β i)] {r : ι → ι → Prop} (hwf : WellFounded r) {x : (i : ι) → β i} {y : (i : ι) → β i} (hlt : x < y) : Pi.Lex r (fun (i : ι) (x x_1 : β i) => x < x_1) x y

theorem Pi.isTrichotomous_lex {ι : Type u_1} {β : ι → Type u_2} (r : ι → ι → Prop) (s : {i : ι} → β i → β i → Prop) [∀ (i : ι), IsTrichotomous (β i) s] (wf : WellFounded r) : IsTrichotomous ((i : ι) → β i) (Pi.Lex r s)

instance Pi.instLTLexForAll {ι : Type u_1} {β : ι → Type u_2} [LT ι] [(a : ι) → LT (β a)] : LT (Lex ((i : ι) → β i))

Equations

• Pi.instLTLexForAll = { lt := Pi.Lex (fun (x x_1 : ι) => x < x_1) fun (x : ι) (x_1 x_2 : β x) => x_1 < x_2 }

instance Pi.Lex.isStrictOrder {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [(a : ι) → PartialOrder (β a)] : IsStrictOrder (Lex ((i : ι) → β i)) fun (x x_1 : Lex ((i : ι) → β i)) => x < x_1

Equations

• ⋯ = ⋯

instance Pi.instPartialOrderLexForAll {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [(a : ι) → PartialOrder (β a)] : PartialOrder (Lex ((i : ι) → β i))

Equations

• Pi.instPartialOrderLexForAll = partialOrderOfSO fun (x x_1 : Lex ((i : ι) → β i)) => x < x_1

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

Πₗ i, α i is a linear order if the original order is well-founded.

Equations

• Pi.instLinearOrderLexForAll = linearOrderOfSTO fun (x x_1 : Lex ((i : ι) → (fun (i : ι) => β i) i)) => x < x_1

theorem Pi.toLex_monotone {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → PartialOrder (β i)] : Monotone ⇑toLex

theorem Pi.toLex_strictMono {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → PartialOrder (β i)] : StrictMono ⇑toLex

@[simp]

theorem Pi.lt_toLex_update_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → PartialOrder (β i)] {x : (i : ι) → β i} {i : ι} {a : β i} : toLex x < toLex (Function.update x i a) ↔ x i < a

@[simp]

theorem Pi.toLex_update_lt_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → PartialOrder (β i)] {x : (i : ι) → β i} {i : ι} {a : β i} : toLex (Function.update x i a) < toLex x ↔ a < x i

@[simp]

theorem Pi.le_toLex_update_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → PartialOrder (β i)] {x : (i : ι) → β i} {i : ι} {a : β i} : toLex x ≤ toLex (Function.update x i a) ↔ x i ≤ a

@[simp]

theorem Pi.toLex_update_le_self_iff {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(i : ι) → PartialOrder (β i)] {x : (i : ι) → β i} {i : ι} {a : β i} : toLex (Function.update x i a) ≤ toLex x ↔ a ≤ x i

instance Pi.instOrderBotLexForAllToLEToPreorderInstPartialOrderLexForAll {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(a : ι) → PartialOrder (β a)] [(a : ι) → OrderBot (β a)] : OrderBot (Lex ((a : ι) → β a))

Equations

• Pi.instOrderBotLexForAllToLEToPreorderInstPartialOrderLexForAll = OrderBot.mk ⋯

instance Pi.instOrderTopLexForAllToLEToPreorderInstPartialOrderLexForAll {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(a : ι) → PartialOrder (β a)] [(a : ι) → OrderTop (β a)] : OrderTop (Lex ((a : ι) → β a))

Equations

• Pi.instOrderTopLexForAllToLEToPreorderInstPartialOrderLexForAll = OrderTop.mk ⋯

instance Pi.instBoundedOrderLexForAllToLEToPreorderInstPartialOrderLexForAll {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [(a : ι) → PartialOrder (β a)] [(a : ι) → BoundedOrder (β a)] : BoundedOrder (Lex ((a : ι) → β a))

Equations

• Pi.instBoundedOrderLexForAllToLEToPreorderInstPartialOrderLexForAll = BoundedOrder.mk

instance Pi.instDenselyOrderedLexForAllInstLTLexForAllToLT {ι : Type u_1} {β : ι → Type u_2} [Preorder ι] [(i : ι) → LT (β i)] [∀ (i : ι), DenselyOrdered (β i)] : DenselyOrdered (Lex ((i : ι) → β i))

Equations

• ⋯ = ⋯

theorem Pi.Lex.noMaxOrder' {ι : Type u_1} {β : ι → Type u_2} [Preorder ι] [(i : ι) → LT (β i)] (i : ι) [NoMaxOrder (β i)] : NoMaxOrder (Lex ((i : ι) → β i))

instance Pi.instNoMaxOrderLexForAllInstLTLexForAllToLTToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLatticeToLTToPreorder {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [Nonempty ι] [(i : ι) → PartialOrder (β i)] [∀ (i : ι), NoMaxOrder (β i)] : NoMaxOrder (Lex ((i : ι) → β i))

Equations

• ⋯ = ⋯

instance Pi.instNoMinOrderLexForAllInstLTLexForAllToLTToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLatticeToLTToPreorder {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [IsWellOrder ι fun (x x_1 : ι) => x < x_1] [Nonempty ι] [(i : ι) → PartialOrder (β i)] [∀ (i : ι), NoMinOrder (β i)] : NoMinOrder (Lex ((i : ι) → β i))

Equations

• ⋯ = ⋯

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 : (fun (i : ι) => β i) x) => x_3 < x_4) i (x i) (x_1 i)), motive ⋯) → motive x_2

Equations

• ⋯ = ⋯

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

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 : (fun (i : ι) => β i) x) => x_4 < x_5) i ((x + x_1) i) ((x + x_2) i)), motive ⋯) → motive x_3

Equations

• ⋯ = ⋯

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

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

Equations

• Pi.Lex.orderedCancelCommMonoid = OrderedCancelCommMonoid.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.orderedAddCommGroup {ι : Type u_1} {β : ι → Type u_2} [LinearOrder ι] [(i : ι) → OrderedAddCommGroup (β i)] : OrderedAddCommGroup (Lex ((i : ι) → β i))

Equations

• Pi.Lex.orderedAddCommGroup = OrderedAddCommGroup.mk ⋯

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_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_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

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_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_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_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

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.

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_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

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

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

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_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_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

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 ⋯ ⋯ ⋯

theorem Pi.lex_desc {ι : Type u_1} {α : Type u_3} [Preorder ι] [DecidableEq ι] [Preorder α] {f : ι → α} {i : ι} {j : ι} (h₁ : i ≤ j) (h₂ : f j < f i) : toLex (f ∘ ⇑(Equiv.swap i j)) < toLex f

If we swap two strictly decreasing values in a function, then the result is lexicographically smaller than the original function.