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 → α i → Prop) : (i : ι) × α i → (i : ι) × α i → Prop

• left: ∀ {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} {i j : ι} (a : α i) (b : α j), r i j → Sigma.Lex r s { fst := i, snd := a } { fst := j, snd := b }
• right: ∀ {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} {i : ι} (a b : α i), s i a b → Sigma.Lex r s { fst := i, snd := a } { fst := i, snd := b }

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.

theorem Sigma.lex_iff {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} {a : (i : ι) × α i} {b : (i : ι) × α i} : Sigma.Lex r s a b ↔ r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd

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 (Sigma.Lex r s)

Equations

• Sigma.Lex.decidable r s x x = decidable_of_decidable_of_iff (_ : (r x.fst x.fst ∨ ∃ h, s x.fst (h ▸ x.snd) x.snd) ↔ Sigma.Lex r s x x)

theorem Sigma.Lex.mono {ι : Type u_1} {α : ι → Type u_2} {r₁ : ι → ι → Prop} {r₂ : ι → ι → Prop} {s₁ : (i : ι) → α i → α i → Prop} {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 : (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 → α i → Prop} (hr : (a b : ι) → r₁ a b → r₂ 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 → α i → Prop} {s₂ : (i : ι) → α i → α i → Prop} (hs : (i : ι) → (a b : α i) → s₁ i a b → s₂ 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 → α i → Prop} {a : (i : ι) × α i} {b : (i : ι) × α i} : Sigma.Lex (Function.swap r) s a b ↔ Sigma.Lex r (fun i => Function.swap (s i)) b a

instance Sigma.instIsReflSigmaLex {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [∀ (i : ι), IsRefl (α i) (s i)] : IsRefl ((i : ι) × α i) (Sigma.Lex r s)

Equations

• @Sigma.instIsReflSigmaLex = @Sigma.instIsReflSigmaLex.proof_1

instance Sigma.instIsIrreflSigmaLex {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [IsIrrefl ι r] [∀ (i : ι), IsIrrefl (α i) (s i)] : IsIrrefl ((i : ι) × α i) (Sigma.Lex r s)

Equations

• @Sigma.instIsIrreflSigmaLex = @Sigma.instIsIrreflSigmaLex.proof_1

instance Sigma.instIsTransSigmaLex {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [IsTrans ι r] [∀ (i : ι), IsTrans (α i) (s i)] : IsTrans ((i : ι) × α i) (Sigma.Lex r s)

Equations

• @Sigma.instIsTransSigmaLex = @Sigma.instIsTransSigmaLex.proof_1

instance Sigma.instIsSymmSigmaLex {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [IsSymm ι r] [∀ (i : ι), IsSymm (α i) (s i)] : IsSymm ((i : ι) × α i) (Sigma.Lex r s)

Equations

• @Sigma.instIsSymmSigmaLex = @Sigma.instIsSymmSigmaLex.proof_1

instance Sigma.instIsAntisymmSigmaLex {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [IsAsymm ι r] [∀ (i : ι), IsAntisymm (α i) (s i)] : IsAntisymm ((i : ι) × α i) (Sigma.Lex r s)

Equations

• @Sigma.instIsAntisymmSigmaLex = @Sigma.instIsAntisymmSigmaLex.proof_1

instance Sigma.instIsTotalSigmaLex {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [IsTrichotomous ι r] [∀ (i : ι), IsTotal (α i) (s i)] : IsTotal ((i : ι) × α i) (Sigma.Lex r s)

Equations

• @Sigma.instIsTotalSigmaLex = @Sigma.instIsTotalSigmaLex.proof_1

instance Sigma.instIsTrichotomousSigmaLex {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [IsTrichotomous ι r] [∀ (i : ι), IsTrichotomous (α i) (s i)] : IsTrichotomous ((i : ι) × α i) (Sigma.Lex r s)

Equations

• @Sigma.instIsTrichotomousSigmaLex = @Sigma.instIsTrichotomousSigmaLex.proof_1

PSigma

theorem PSigma.lex_iff {ι : Sort u_1} {α : ι → Sort u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} {a : (i : ι) ×' α i} {b : (i : ι) ×' α i} : PSigma.Lex r s a b ↔ r a.fst b.fst ∨ ∃ h, s b.fst (h ▸ a.snd) b.snd

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 (PSigma.Lex r s)

Equations

• PSigma.Lex.decidable r s x x = decidable_of_decidable_of_iff (_ : (r x.fst x.fst ∨ ∃ h, s x.fst (h ▸ x.snd) x.snd) ↔ PSigma.Lex r s x x)

theorem PSigma.Lex.mono {ι : Sort u_1} {α : ι → Sort u_2} {r₁ : ι → ι → Prop} {r₂ : ι → ι → Prop} {s₁ : (i : ι) → α i → α i → Prop} {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 : (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 → α i → Prop} (hr : (a b : ι) → r₁ a b → r₂ 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 → α i → Prop} {s₂ : (i : ι) → α i → α i → Prop} (hs : (i : ι) → (a b : α i) → s₁ i a b → s₂ i a b) {a : (i : ι) ×' α i} {b : (i : ι) ×' α i} (h : PSigma.Lex r s₁ a b) : PSigma.Lex r s₂ a b