mathlib documentation

data.sigma.lex

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:

data.finset.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) (a b : Σ (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 ⟨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 → sigma.lex r s ⟨i, a⟩ ⟨i, 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.

Instances for sigma.lex

theorem sigma.lex_iff {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : Π (i : ι), α i → α i → Prop} {a b : Σ (i : ι), α i} :

sigma.lex r s a b ↔ r a.fst b.fst ∨ ∃ (h : a.fst = b.fst), s b.fst (eq.rec a.snd h) b.snd

@[protected, instance]

def sigma.lex.decidable {ι : Type u_1} {α : ι → Type u_2} (r : ι → ι → Prop) (s : Π (i : ι), α i → α i → Prop) [decidable_eq ι] [decidable_rel r] [Π (i : ι), decidable_rel (s i)] :

decidable_rel (sigma.lex r s)

Equations

sigma.lex.decidable r s = λ (a b : Σ (i : ι), α i), decidable_of_decidable_of_iff infer_instance _

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 : sigma.lex r₁ s₁ a b) :

sigma.lex r₂ s₂ a b

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 : 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₁ s₂ : Π (i : ι), α i → α i → Prop} (hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b) {a b : Σ (i : ι), α i} (h : sigma.lex r s₁ a b) :

sigma.lex r s₂ a b

@[protected, instance]

def sigma.lex.is_refl {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : Π (i : ι), α i → α i → Prop} [∀ (i : ι), is_refl (α i) (s i)] :

is_refl (Σ (i : ι), α i) (sigma.lex r s)

@[protected, instance]

def sigma.lex.is_irrefl {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : Π (i : ι), α i → α i → Prop} [is_irrefl ι r] [∀ (i : ι), is_irrefl (α i) (s i)] :

is_irrefl (Σ (i : ι), α i) (sigma.lex r s)

@[protected, instance]

def sigma.lex.is_trans {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : Π (i : ι), α i → α i → Prop} [is_trans ι r] [∀ (i : ι), is_trans (α i) (s i)] :

is_trans (Σ (i : ι), α i) (sigma.lex r s)

@[protected, instance]

def sigma.lex.is_symm {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : Π (i : ι), α i → α i → Prop} [is_symm ι r] [∀ (i : ι), is_symm (α i) (s i)] :

is_symm (Σ (i : ι), α i) (sigma.lex r s)

@[protected, instance]

def sigma.lex.is_antisymm {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : Π (i : ι), α i → α i → Prop} [is_asymm ι r] [∀ (i : ι), is_antisymm (α i) (s i)] :

is_antisymm (Σ (i : ι), α i) (sigma.lex r s)

@[protected, instance]

def sigma.lex.is_total {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : Π (i : ι), α i → α i → Prop} [is_trichotomous ι r] [∀ (i : ι), is_total (α i) (s i)] :

is_total (Σ (i : ι), α i) (sigma.lex r s)

@[protected, instance]

def sigma.lex.is_trichotomous {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : Π (i : ι), α i → α i → Prop} [is_trichotomous ι r] [∀ (i : ι), is_trichotomous (α i) (s i)] :

is_trichotomous (Σ (i : ι), α i) (sigma.lex r s)

`psigma` #

theorem psigma.lex_iff {ι : Sort u_1} {α : ι → Sort u_2} {r : ι → ι → Prop} {s : Π (i : ι), α i → α i → Prop} {a b : Σ' (i : ι), α i} :

psigma.lex r s a b ↔ r a.fst b.fst ∨ ∃ (h : a.fst = b.fst), s b.fst (eq.rec a.snd h) b.snd

@[protected, instance]

def psigma.lex.decidable {ι : Sort u_1} {α : ι → Sort u_2} (r : ι → ι → Prop) (s : Π (i : ι), α i → α i → Prop) [decidable_eq ι] [decidable_rel r] [Π (i : ι), decidable_rel (s i)] :

decidable_rel (psigma.lex r s)

Equations

psigma.lex.decidable r s = λ (a b : Σ' (i : ι), α i), decidable_of_decidable_of_iff infer_instance _

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 : psigma.lex r₁ s₁ a b) :

psigma.lex r₂ s₂ a b

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 : 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₁ s₂ : Π (i : ι), α i → α i → Prop} (hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b) {a b : Σ' (i : ι), α i} (h : psigma.lex r s₁ a b) :

psigma.lex r s₂ a b