# 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

source
inductive Sigma.Lex {ι : Type u_1} {α : ι → Type u_2} (r : ι → ι → Prop) (s : (i : ι) → α i → α i → Prop) :
(i : ι) × α i → (i : ι) × α i → Prop

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 → α i → Prop} {i j : ι} (a : α i) (b : α j) : r i j → Lex r s ⟨i, a⟩ ⟨j, b⟩
- right {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} {i : ι} (a b : α i) : s i a b → Lex r s ⟨i, a⟩ ⟨i, b⟩

Instances For

source
theorem Sigma.lex_iff {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} {a b : (i : ι) × α i} :
Lex r s a b ↔ r a.fst b.fst ∨ ∃ (h : a.fst = b.fst), s b.fst (h ▸ a.snd) b.snd
source
instance Sigma.Lex.decidable {ι : Type u_1} {α : ι → Type u_2} (r : ι → ι → Prop) (s : (i : ι) → α i → α i → Prop) [DecidableEq ι] [DecidableRel r] [(i : ι) → DecidableRel (s i)] :
DecidableRel (Lex r s)
Equations

- Sigma.Lex.decidable r s x✝¹ x✝ = decidable_of_decidable_of_iff ⋯

source
theorem Sigma.Lex.mono {ι : Type u_1} {α : ι → Type u_2} {r₁ r₂ : ι → ι → Prop} {s₁ s₂ : (i : ι) → α i → α i → Prop} (hr : ∀ (a b : ι), r₁ a b → r₂ a b) (hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b) {a b : (i : ι) × α i} (h : Lex r₁ s₁ a b) :
Lex r₂ s₂ a b
source
theorem Sigma.Lex.mono_left {ι : Type u_1} {α : ι → Type u_2} {r₁ r₂ : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} (hr : ∀ (a b : ι), r₁ a b → r₂ a b) {a b : (i : ι) × α i} (h : Lex r₁ s a b) :
Lex r₂ s a b
source
theorem Sigma.Lex.mono_right {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s₁ s₂ : (i : ι) → α i → α i → Prop} (hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b) {a b : (i : ι) × α i} (h : Lex r s₁ a b) :
Lex r s₂ a b
source
theorem Sigma.lex_swap {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} {a b : (i : ι) × α i} :
Lex (Function.swap r) s a b ↔ Lex r (fun (i : ι) => Function.swap (s i)) b a
source
instance Sigma.instIsReflLex {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [∀ (i : ι), IsRefl (α i) (s i)] :
IsRefl ((i : ι) × α i) (Lex r s)
source
instance Sigma.instIsIrreflLex {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [IsIrrefl ι r] [∀ (i : ι), IsIrrefl (α i) (s i)] :
IsIrrefl ((i : ι) × α i) (Lex r s)
source
instance Sigma.instIsTransLex {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [IsTrans ι r] [∀ (i : ι), IsTrans (α i) (s i)] :
IsTrans ((i : ι) × α i) (Lex r s)
source
instance Sigma.instIsSymmLex {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [IsSymm ι r] [∀ (i : ι), IsSymm (α i) (s i)] :
IsSymm ((i : ι) × α i) (Lex r s)
source
instance Sigma.instIsAntisymmLexOfIsAsymm {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [IsAsymm ι r] [∀ (i : ι), IsAntisymm (α i) (s i)] :
IsAntisymm ((i : ι) × α i) (Lex r s)
source
instance Sigma.instIsTotalLexOfIsTrichotomous {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [IsTrichotomous ι r] [∀ (i : ι), IsTotal (α i) (s i)] :
IsTotal ((i : ι) × α i) (Lex r s)
source
instance Sigma.instIsTrichotomousLex {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [IsTrichotomous ι r] [∀ (i : ι), IsTrichotomous (α i) (s i)] :
IsTrichotomous ((i : ι) × α i) (Lex r s)

### `PSigma` #

source
theorem PSigma.lex_iff {ι : Sort u_1} {α : ι → Sort u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} {a b : (i : ι) ×' α i} :
Lex r s a b ↔ r a.fst b.fst ∨ ∃ (h : a.fst = b.fst), s b.fst (h ▸ a.snd) b.snd
source
instance PSigma.Lex.decidable {ι : Sort u_1} {α : ι → Sort u_2} (r : ι → ι → Prop) (s : (i : ι) → α i → α i → Prop) [DecidableEq ι] [DecidableRel r] [(i : ι) → DecidableRel (s i)] :
DecidableRel (Lex r s)
Equations

- PSigma.Lex.decidable r s x✝¹ x✝ = decidable_of_decidable_of_iff ⋯

source
theorem PSigma.Lex.mono {ι : Sort u_1} {α : ι → Sort u_2} {r₁ r₂ : ι → ι → Prop} {s₁ s₂ : (i : ι) → α i → α i → Prop} (hr : ∀ (a b : ι), r₁ a b → r₂ a b) (hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b) {a b : (i : ι) ×' α i} (h : Lex r₁ s₁ a b) :
Lex r₂ s₂ a b
source
theorem PSigma.Lex.mono_left {ι : Sort u_1} {α : ι → Sort u_2} {r₁ r₂ : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} (hr : ∀ (a b : ι), r₁ a b → r₂ a b) {a b : (i : ι) ×' α i} (h : Lex r₁ s a b) :
Lex r₂ s a b
source
theorem PSigma.Lex.mono_right {ι : Sort u_1} {α : ι → Sort u_2} {r : ι → ι → Prop} {s₁ s₂ : (i : ι) → α i → α i → Prop} (hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b) {a b : (i : ι) ×' α i} (h : Lex r s₁ a b) :
Lex r s₂ a b