mathlib documentation

core / init.data.sigma.lex

inductive psigma.lex {α : Sort u} {β : α Sort v} (r : α α Prop) (s : Π (a : α), β a β a Prop) :
psigma β psigma β Prop
Instances for psigma.lex
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⟩
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)) :
def psigma.lex_ndep {α : Sort u} {β : Sort v} (r : α α Prop) (s : β β Prop) :
(Σ' (a : α), β) (Σ' (a : α), β) Prop
Equations
theorem psigma.lex_ndep_wf {α : Sort u} {β : Sort v} {r : α α Prop} {s : β β Prop} (ha : well_founded r) (hb : well_founded s) :
inductive psigma.rev_lex {α : Sort u} {β : Sort v} (r : α α Prop) (s : β β Prop) :
(Σ' (a : α), β) (Σ' (a : α), β) Prop
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⟩
theorem psigma.rev_lex_wf {α : Sort u} {β : Sort v} {r : α α Prop} {s : β β Prop} (ha : well_founded r) (hb : well_founded s) :
def psigma.skip_left (α : Type u) {β : Type v} (s : β β Prop) :
(Σ' (a : α), β) (Σ' (a : α), β) Prop
Equations
theorem psigma.skip_left_wf (α : Type u) {β : Type v} {s : β β Prop} (hb : well_founded s) :
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₂⟩
@[protected, instance]
def psigma.has_well_founded {α : Type u} {β : α Type v} [s₁ : has_well_founded α] [s₂ : Π (a : α), has_well_founded (β a)] :
Equations