core / init.data.sigma.lex

inductive psigma.lex {α : Sort u} {β : α → Sort v} (r : α → α → Prop) (s : Π (a : α), β a → β a → Prop) :

left : ∀ {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : Π (a : α), β a → β a → Prop} {a₁ : α} (b₁ : β a₁) {a₂ : α} (b₂ : β a₂), r a₁ a₂ → psigma.lex r s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
right : ∀ {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : Π (a : α), β a → β a → Prop} (a : α) {b₁ b₂ : β a}, s a b₁ b₂ → psigma.lex r s ⟨a, b₁⟩ ⟨a, b₂⟩

Instances for psigma.lex

psigma.lex.decidable

theorem psigma.lex_accessible {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : Π (a : α), β a → β a → Prop} {a : α} (aca : acc r a) (acb : ∀ (a : α), well_founded (s a)) (b : β a) :

acc (psigma.lex r s) ⟨a, b⟩

source

theorem psigma.lex_wf {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : Π (a : α), β a → β a → Prop} (ha : well_founded r) (hb : ∀ (x : α), well_founded (s x)) :

well_founded (psigma.lex r s)

source

def psigma.lex_ndep {α : Sort u} {β : Sort v} (r : α → α → Prop) (s : β → β → Prop) :

(Σ' (a : α), β) → (Σ' (a : α), β) → Prop

Equations

psigma.lex_ndep r s = psigma.lex r (λ (a : α), s)

source

theorem psigma.lex_ndep_wf {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (ha : well_founded r) (hb : well_founded s) :

well_founded (psigma.lex_ndep r s)

source

inductive psigma.rev_lex {α : Sort u} {β : Sort v} (r : α → α → Prop) (s : β → β → Prop) :

(Σ' (a : α), β) → (Σ' (a : α), β) → Prop

left : ∀ {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} {a₁ a₂ : α} (b : β), r a₁ a₂ → psigma.rev_lex r s ⟨a₁, b⟩ ⟨a₂, b⟩
right : ∀ {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β}, s b₁ b₂ → psigma.rev_lex r s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩

source

theorem psigma.rev_lex_accessible {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} {b : β} (acb : acc s b) (aca : ∀ (a : α), acc r a) (a : α) :

acc (psigma.rev_lex r s) ⟨a, b⟩

source

theorem psigma.rev_lex_wf {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (ha : well_founded r) (hb : well_founded s) :

well_founded (psigma.rev_lex r s)

source

def psigma.skip_left (α : Type u) {β : Type v} (s : β → β → Prop) :

(Σ' (a : α), β) → (Σ' (a : α), β) → Prop

Equations

psigma.skip_left α s = psigma.rev_lex empty_relation s

source

theorem psigma.skip_left_wf (α : Type u) {β : Type v} {s : β → β → Prop} (hb : well_founded s) :

well_founded (psigma.skip_left α s)

source

theorem psigma.mk_skip_left {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} (a₁ a₂ : α) (h : s b₁ b₂) :

psigma.skip_left α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩

source

@[protected, instance]

def psigma.has_well_founded {α : Type u} {β : α → Type v} [s₁ : has_well_founded α] [s₂ : Π (a : α), has_well_founded (β a)] :

has_well_founded (psigma β)

Equations

psigma.has_well_founded = {r := psigma.lex has_well_founded.r (λ (a : α), has_well_founded.r), wf := _}