Documentation

Mathlib.Init.Data.Sigma.Lex

Well-foundedness of orders of well-founded relations #

Porting note: many declarations that were here in mathlib3 have been moved to Init.WF in Lean 4 core. The ones below are all the exceptions.

theorem PSigma.lex_wf {α : Sort u} {β : αSort v} {r : ααProp} {s : (a : α) → β aβ aProp} (ha : WellFounded r) (hb : ∀ (x : α), WellFounded (s x)) :

The lexicographical order of well-founded relations is well-founded.

theorem PSigma.revLex_wf {α : Sort u} {β : Sort v} {r : ααProp} {s : ββProp} (ha : WellFounded r) (hb : WellFounded s) :
theorem PSigma.skipLeft_wf (α : Type u) {β : Type v} {s : ββProp} (hb : WellFounded s) :
instance PSigma.hasWellFounded {α : Type u} {β : αType v} [s₁ : WellFoundedRelation α] [s₂ : (a : α) → WellFoundedRelation (β a)] :