Documentation

Mathlib.Data.Pi.Lex

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 #

See also #

Related files are:

instance Pi.instForAllInhabitedLex {α : Type u_1} [inst : Inhabited α] :
Equations
  • Pi.instForAllInhabitedLex = x
def Pi.Lex {ι : Type u_1} {β : ιType u_2} (r : ιιProp) (s : {i : ι} → β iβ iProp) (x : (i : ι) → β i) (y : (i : ι) → β i) :

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 ix j = y j) s i (x i) (y i)

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_2} {β : ιType u_1} (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_2} {β : ιType u_1} [inst : (i : ι) → Preorder (β i)] {r : ιιProp} (hwf : WellFounded r) {x : (i : ι) → β i} {y : (i : ι) → β i} (hlt : x < y) :
i, (∀ (j : ι), r j ix j y j y j x j) x i < y i
theorem Pi.lex_lt_of_lt {ι : Type u_2} {β : ιType u_1} [inst : (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 => x < x_1) x y
theorem Pi.isTrichotomous_lex {ι : Type u_2} {β : ιType u_1} (r : ιιProp) (s : {i : ι} → β iβ iProp) [inst : ∀ (i : ι), IsTrichotomous (β i) (s i)] (wf : WellFounded r) :
IsTrichotomous ((i : ι) → β i) (Pi.Lex r s)
instance Pi.instLTLexForAll {ι : Type u_1} {β : ιType u_2} [inst : LT ι] [inst : (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_1 < x_2 }
instance Pi.Lex.isStrictOrder {ι : Type u_1} {β : ιType u_2} [inst : LinearOrder ι] [inst : (a : ι) → PartialOrder (β a)] :
IsStrictOrder (Lex ((i : ι) → β i)) fun x x_1 => x < x_1
Equations
instance Pi.instPartialOrderLexForAll {ι : Type u_1} {β : ιType u_2} [inst : LinearOrder ι] [inst : (a : ι) → PartialOrder (β a)] :
PartialOrder (Lex ((i : ι) → β i))
Equations
noncomputable instance Pi.instLinearOrderLexForAll {ι : Type u_1} {β : ιType u_2} [inst : LinearOrder ι] [inst : IsWellOrder ι fun x x_1 => x < x_1] [inst : (a : ι) → LinearOrder (β a)] :
LinearOrder (Lex ((i : ι) → β i))

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

Equations
theorem Pi.toLex_monotone {ι : Type u_1} {β : ιType u_2} [inst : LinearOrder ι] [inst : IsWellOrder ι fun x x_1 => x < x_1] [inst : (i : ι) → PartialOrder (β i)] :
Monotone toLex
theorem Pi.toLex_strictMono {ι : Type u_1} {β : ιType u_2} [inst : LinearOrder ι] [inst : IsWellOrder ι fun x x_1 => x < x_1] [inst : (i : ι) → PartialOrder (β i)] :
StrictMono toLex
@[simp]
theorem Pi.lt_toLex_update_self_iff {ι : Type u_1} {β : ιType u_2} [inst : LinearOrder ι] [inst : IsWellOrder ι fun x x_1 => x < x_1] [inst : (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} [inst : LinearOrder ι] [inst : IsWellOrder ι fun x x_1 => x < x_1] [inst : (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} [inst : LinearOrder ι] [inst : IsWellOrder ι fun x x_1 => x < x_1] [inst : (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} [inst : LinearOrder ι] [inst : IsWellOrder ι fun x x_1 => x < x_1] [inst : (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} [inst : LinearOrder ι] [inst : IsWellOrder ι fun x x_1 => x < x_1] [inst : (a : ι) → PartialOrder (β a)] [inst : (a : ι) → OrderBot (β a)] :
OrderBot (Lex ((a : ι) → β a))
Equations
  • Pi.instOrderBotLexForAllToLEToPreorderInstPartialOrderLexForAll = OrderBot.mk (_ : ∀ (x : Lex ((a : ι) → β a)), toLex toLex x)
instance Pi.instOrderTopLexForAllToLEToPreorderInstPartialOrderLexForAll {ι : Type u_1} {β : ιType u_2} [inst : LinearOrder ι] [inst : IsWellOrder ι fun x x_1 => x < x_1] [inst : (a : ι) → PartialOrder (β a)] [inst : (a : ι) → OrderTop (β a)] :
OrderTop (Lex ((a : ι) → β a))
Equations
  • Pi.instOrderTopLexForAllToLEToPreorderInstPartialOrderLexForAll = OrderTop.mk (_ : ∀ (x : Lex ((a : ι) → β a)), toLex x toLex )
instance Pi.instBoundedOrderLexForAllToLEToPreorderInstPartialOrderLexForAll {ι : Type u_1} {β : ιType u_2} [inst : LinearOrder ι] [inst : IsWellOrder ι fun x x_1 => x < x_1] [inst : (a : ι) → PartialOrder (β a)] [inst : (a : ι) → BoundedOrder (β a)] :
BoundedOrder (Lex ((a : ι) → β a))
Equations
  • Pi.instBoundedOrderLexForAllToLEToPreorderInstPartialOrderLexForAll = BoundedOrder.mk
instance Pi.instDenselyOrderedLexForAllInstLTLexForAllToLT {ι : Type u_1} {β : ιType u_2} [inst : Preorder ι] [inst : (i : ι) → LT (β i)] [inst : ∀ (i : ι), DenselyOrdered (β i)] :
DenselyOrdered (Lex ((i : ι) → β i))
Equations
theorem Pi.Lex.noMaxOrder' {ι : Type u_1} {β : ιType u_2} [inst : Preorder ι] [inst : (i : ι) → LT (β i)] (i : ι) [inst : NoMaxOrder (β i)] :
NoMaxOrder (Lex ((i : ι) → β i))
instance Pi.instNoMaxOrderLexForAllInstLTLexForAllToLTToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLatticeToLTToPreorder {ι : Type u_1} {β : ιType u_2} [inst : LinearOrder ι] [inst : IsWellOrder ι fun x x_1 => x < x_1] [inst : Nonempty ι] [inst : (i : ι) → PartialOrder (β i)] [inst : ∀ (i : ι), NoMaxOrder (β i)] :
NoMaxOrder (Lex ((i : ι) → β i))
Equations
  • One or more equations did not get rendered due to their size.
instance Pi.instNoMinOrderLexForAllInstLTLexForAllToLTToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLatticeToLTToPreorder {ι : Type u_1} {β : ιType u_2} [inst : LinearOrder ι] [inst : IsWellOrder ι fun x x_1 => x < x_1] [inst : Nonempty ι] [inst : (i : ι) → PartialOrder (β i)] [inst : ∀ (i : ι), NoMinOrder (β i)] :
NoMinOrder (Lex ((i : ι) → β i))
Equations
  • One or more equations did not get rendered due to their size.
instance Pi.Lex.orderedAddCommGroup {ι : Type u_1} {β : ιType u_2} [inst : LinearOrder ι] [inst : (a : ι) → OrderedAddCommGroup (β a)] :
OrderedAddCommGroup (Lex ((i : ι) → β i))
Equations
  • Pi.Lex.orderedAddCommGroup = let src := Pi.addCommGroup; OrderedAddCommGroup.mk (_ : ∀ (x y : Lex ((i : ι) → β i)), x y∀ (z : Lex ((i : ι) → β i)), z + x z + y)
def Pi.Lex.orderedAddCommGroup.proof_1 {ι : Type u_1} {β : ιType u_2} [inst : (a : ι) → OrderedAddCommGroup (β a)] (a : (i : ι) → β i) (b : (i : ι) → β i) :
a + b = b + a
Equations
  • (_ : ∀ (a b : (i : ι) → β i), a + b = b + a) = (_ : ∀ (a b : (i : ι) → β i), a + b = b + a)
def Pi.Lex.orderedAddCommGroup.proof_2 {ι : Type u_1} {β : ιType u_2} [inst : LinearOrder ι] [inst : (a : ι) → OrderedAddCommGroup (β a)] (x : Lex ((i : ι) → β i)) (y : Lex ((i : ι) → β i)) (hxy : x y) (z : Lex ((i : ι) → β i)) :
z + x z + y
Equations
abbrev Pi.Lex.orderedAddCommGroup.match_1 {ι : Type u_1} {β : ιType u_2} [inst : LinearOrder ι] [inst : (a : ι) → OrderedAddCommGroup (β a)] (x : Lex ((i : ι) → β i)) (y : Lex ((i : ι) → β i)) (motive : x < yProp) :
(x : x < y) → ((i : ι) → (hi : (∀ (j : ι), j < ix j = y j) (fun x x_1 x_2 => x_1 < x_2) i (x i) (y i)) → motive (_ : i, (∀ (j : ι), j < ix j = y j) (fun x x_1 x_2 => x_1 < x_2) i (x i) (y i))) → motive x
Equations
instance Pi.Lex.orderedCommGroup {ι : Type u_1} {β : ιType u_2} [inst : LinearOrder ι] [inst : (a : ι) → OrderedCommGroup (β a)] :
OrderedCommGroup (Lex ((i : ι) → β i))
Equations
  • Pi.Lex.orderedCommGroup = let src := Pi.commGroup; OrderedCommGroup.mk (_ : ∀ (x y : Lex ((i : ι) → β i)), x y∀ (z : Lex ((i : ι) → β i)), z * x z * y)
theorem Pi.lex_desc {ι : Type u_2} {α : Type u_1} [inst : Preorder ι] [inst : DecidableEq ι] [inst : 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.