# Lexicographic order on a sigma type #

This defines the lexicographical order of two arbitrary relations on a sigma type and proves some lemmas about PSigma.Lex, which is defined in core Lean.

Given a relation in the index type and a relation on each summand, the lexicographical order on the sigma type relates a and b if their summands are related or they are in the same summand and related by the summand's relation.

## See also #

Related files are:

• Combinatorics.CoLex: Colexicographic order on finite sets.
• Data.List.Lex: Lexicographic order on lists.
• Data.Sigma.Order: Lexicographic order on Σ i, α i per say.
• Data.PSigma.Order: Lexicographic order on Σ' i, α i.
• Data.Prod.Lex: Lexicographic order on α × β. Can be thought of as the special case of Sigma.Lex where all summands are the same
inductive Sigma.Lex {ι : Type u_1} {α : ιType u_2} (r : ιιProp) (s : (i : ι) → α iα iProp) :
(i : ι) × α i(i : ι) × α iProp

The lexicographical order on a sigma type. It takes in a relation on the index type and a relation for each summand. a is related to b iff their summands are related or they are in the same summand and are related through the summand's relation.

• left: ∀ {ι : Type u_1} {α : ιType u_2} {r : ιιProp} {s : (i : ι) → α iα iProp} {i j : ι} (a : α i) (b : α j), r i jSigma.Lex r s i, a j, b
• right: ∀ {ι : Type u_1} {α : ιType u_2} {r : ιιProp} {s : (i : ι) → α iα iProp} {i : ι} (a b : α i), s i a bSigma.Lex r s i, a i, b
Instances For
theorem Sigma.lex_iff {ι : Type u_1} {α : ιType u_2} {r : ιιProp} {s : (i : ι) → α iα iProp} {a : (i : ι) × α i} {b : (i : ι) × α i} :
Sigma.Lex r s a b r a.fst b.fst ∃ (h : a.fst = b.fst), s b.fst (ha.snd) b.snd
instance Sigma.Lex.decidable {ι : Type u_1} {α : ιType u_2} (r : ιιProp) (s : (i : ι) → α iα iProp) [] [] [(i : ι) → DecidableRel (s i)] :
Equations
theorem Sigma.Lex.mono {ι : Type u_1} {α : ιType u_2} {r₁ : ιιProp} {r₂ : ιιProp} {s₁ : (i : ι) → α iα iProp} {s₂ : (i : ι) → α iα iProp} (hr : ∀ (a b : ι), r₁ a br₂ a b) (hs : ∀ (i : ι) (a b : α i), s₁ i a bs₂ i a b) {a : (i : ι) × α i} {b : (i : ι) × α i} (h : Sigma.Lex r₁ s₁ a b) :
Sigma.Lex r₂ s₂ a b
theorem Sigma.Lex.mono_left {ι : Type u_1} {α : ιType u_2} {r₁ : ιιProp} {r₂ : ιιProp} {s : (i : ι) → α iα iProp} (hr : ∀ (a b : ι), r₁ a br₂ a b) {a : (i : ι) × α i} {b : (i : ι) × α i} (h : Sigma.Lex r₁ s a b) :
Sigma.Lex r₂ s a b
theorem Sigma.Lex.mono_right {ι : Type u_1} {α : ιType u_2} {r : ιιProp} {s₁ : (i : ι) → α iα iProp} {s₂ : (i : ι) → α iα iProp} (hs : ∀ (i : ι) (a b : α i), s₁ i a bs₂ i a b) {a : (i : ι) × α i} {b : (i : ι) × α i} (h : Sigma.Lex r s₁ a b) :
Sigma.Lex r s₂ a b
theorem Sigma.lex_swap {ι : Type u_1} {α : ιType u_2} {r : ιιProp} {s : (i : ι) → α iα iProp} {a : (i : ι) × α i} {b : (i : ι) × α i} :
Sigma.Lex s a b Sigma.Lex r (fun (i : ι) => Function.swap (s i)) b a
instance Sigma.instIsReflLex {ι : Type u_1} {α : ιType u_2} {r : ιιProp} {s : (i : ι) → α iα iProp} [∀ (i : ι), IsRefl (α i) (s i)] :
IsRefl ((i : ι) × α i) (Sigma.Lex r s)
Equations
• =
instance Sigma.instIsIrreflLex {ι : Type u_1} {α : ιType u_2} {r : ιιProp} {s : (i : ι) → α iα iProp} [IsIrrefl ι r] [∀ (i : ι), IsIrrefl (α i) (s i)] :
IsIrrefl ((i : ι) × α i) (Sigma.Lex r s)
Equations
• =
instance Sigma.instIsTransLex {ι : Type u_1} {α : ιType u_2} {r : ιιProp} {s : (i : ι) → α iα iProp} [IsTrans ι r] [∀ (i : ι), IsTrans (α i) (s i)] :
IsTrans ((i : ι) × α i) (Sigma.Lex r s)
Equations
• =
instance Sigma.instIsSymmLex {ι : Type u_1} {α : ιType u_2} {r : ιιProp} {s : (i : ι) → α iα iProp} [IsSymm ι r] [∀ (i : ι), IsSymm (α i) (s i)] :
IsSymm ((i : ι) × α i) (Sigma.Lex r s)
Equations
• =
instance Sigma.instIsAntisymmLexOfIsAsymm {ι : Type u_1} {α : ιType u_2} {r : ιιProp} {s : (i : ι) → α iα iProp} [IsAsymm ι r] [∀ (i : ι), IsAntisymm (α i) (s i)] :
IsAntisymm ((i : ι) × α i) (Sigma.Lex r s)
Equations
• =
instance Sigma.instIsTotalLexOfIsTrichotomous {ι : Type u_1} {α : ιType u_2} {r : ιιProp} {s : (i : ι) → α iα iProp} [] [∀ (i : ι), IsTotal (α i) (s i)] :
IsTotal ((i : ι) × α i) (Sigma.Lex r s)
Equations
• =
instance Sigma.instIsTrichotomousLex {ι : Type u_1} {α : ιType u_2} {r : ιιProp} {s : (i : ι) → α iα iProp} [] [∀ (i : ι), IsTrichotomous (α i) (s i)] :
IsTrichotomous ((i : ι) × α i) (Sigma.Lex r s)
Equations
• =

### PSigma#

theorem PSigma.lex_iff {ι : Sort u_1} {α : ιSort u_2} {r : ιιProp} {s : (i : ι) → α iα iProp} {a : (i : ι) ×' α i} {b : (i : ι) ×' α i} :
PSigma.Lex r s a b r a.fst b.fst ∃ (h : a.fst = b.fst), s b.fst (ha.snd) b.snd
instance PSigma.Lex.decidable {ι : Sort u_1} {α : ιSort u_2} (r : ιιProp) (s : (i : ι) → α iα iProp) [] [] [(i : ι) → DecidableRel (s i)] :
Equations
theorem PSigma.Lex.mono {ι : Sort u_1} {α : ιSort u_2} {r₁ : ιιProp} {r₂ : ιιProp} {s₁ : (i : ι) → α iα iProp} {s₂ : (i : ι) → α iα iProp} (hr : ∀ (a b : ι), r₁ a br₂ a b) (hs : ∀ (i : ι) (a b : α i), s₁ i a bs₂ i a b) {a : (i : ι) ×' α i} {b : (i : ι) ×' α i} (h : PSigma.Lex r₁ s₁ a b) :
PSigma.Lex r₂ s₂ a b
theorem PSigma.Lex.mono_left {ι : Sort u_1} {α : ιSort u_2} {r₁ : ιιProp} {r₂ : ιιProp} {s : (i : ι) → α iα iProp} (hr : ∀ (a b : ι), r₁ a br₂ a b) {a : (i : ι) ×' α i} {b : (i : ι) ×' α i} (h : PSigma.Lex r₁ s a b) :
PSigma.Lex r₂ s a b
theorem PSigma.Lex.mono_right {ι : Sort u_1} {α : ιSort u_2} {r : ιιProp} {s₁ : (i : ι) → α iα iProp} {s₂ : (i : ι) → α iα iProp} (hs : ∀ (i : ι) (a b : α i), s₁ i a bs₂ i a b) {a : (i : ι) ×' α i} {b : (i : ι) ×' α i} (h : PSigma.Lex r s₁ a b) :
PSigma.Lex r s₂ a b