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 → β a → Prop}
(ha : WellFounded r)
(hb : ∀ (x : α), WellFounded (s x))
:
WellFounded (PSigma.Lex r s)
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)
:
WellFounded (PSigma.RevLex r s)
theorem
PSigma.skipLeft_wf
(α : Type u)
{β : Type v}
{s : β → β → Prop}
(hb : WellFounded s)
:
WellFounded (PSigma.SkipLeft α s)
instance
PSigma.hasWellFounded
{α : Type u}
{β : α → Type v}
[s₁ : WellFoundedRelation α]
[s₂ : (a : α) → WellFoundedRelation (β a)]
:
Equations
- PSigma.hasWellFounded = { rel := PSigma.Lex WellFoundedRelation.rel fun (a : α) => WellFoundedRelation.rel, wf := ⋯ }