A relation r
is WellFounded
if all elements of α
are accessible within r
.
If a relation is WellFounded
, it does not allow for an infinite descent along the relation.
If the arguments of the recursive calls in a function definition decrease according to a well founded relation, then the function terminates. Well-founded relations are sometimes called Artinian or said to satisfy the “descending chain condition”.
- intro: ∀ {α : Sort u} {r : α → α → Prop}, (∀ (a : α), Acc r a) → WellFounded r
- rel : α → α → Prop
- wf : WellFounded WellFoundedRelation.rel
Instances
- Acc.wfRel
- Cardinal.instWellFoundedRelation
- ENat.instWellFoundedRelation
- Fin.instWellFoundedRelation_mathlib
- Finsupp.instWellFoundedRelationNat
- Nat.WithBot.instWellFoundedRelationWithBot
- Ordinal.wellFoundedRelation
- PNat.instWellFoundedRelation
- PSigma.instWellFoundedRelation
- PartENat.wellFoundedRelation
- Polynomial.instWellFoundedRelation
- Prod.Lex.instWellFoundedRelationLexOfWellFoundedLT
- Prod.instWellFoundedRelation
- hasWellFounded_toType
- instENatWellFoundedRelation
- instWellFoundedRelationOfSizeOf
- instWellFoundedRelationWithTopNat
noncomputable def
WellFounded.recursion
{α : Sort u}
{r : α → α → Prop}
(hwf : WellFounded r)
{C : α → Sort v}
(a : α)
(h : (x : α) → ((y : α) → r y x → C y) → C x)
:
C a
theorem
WellFounded.induction
{α : Sort u}
{r : α → α → Prop}
(hwf : WellFounded r)
{C : α → Prop}
(a : α)
(h : ∀ (x : α), (∀ (y : α), r y x → C y) → C x)
:
C a
noncomputable def
WellFounded.fixF
{α : Sort u}
{r : α → α → Prop}
{C : α → Sort v}
(F : (x : α) → ((y : α) → r y x → C y) → C x)
(x : α)
(a : Acc r x)
:
C x
Equations
- WellFounded.fixF F x a = Acc.rec (fun (x₁ : α) (h : ∀ (y : α), r y x₁ → Acc r y) (ih : (y : α) → r y x₁ → C y) => F x₁ ih) a
theorem
WellFounded.fixFEq
{α : Sort u}
{r : α → α → Prop}
{C : α → Sort v}
(F : (x : α) → ((y : α) → r y x → C y) → C x)
(x : α)
(acx : Acc r x)
:
WellFounded.fixF F x acx = F x fun (y : α) (p : r y x) => WellFounded.fixF F y ⋯
noncomputable def
WellFounded.fix
{α : Sort u}
{C : α → Sort v}
{r : α → α → Prop}
(hwf : WellFounded r)
(F : (x : α) → ((y : α) → r y x → C y) → C x)
(x : α)
:
C x
Equations
- hwf.fix F x = WellFounded.fixF F x ⋯
theorem
WellFounded.fix_eq
{α : Sort u}
{C : α → Sort v}
{r : α → α → Prop}
(hwf : WellFounded r)
(F : (x : α) → ((y : α) → r y x → C y) → C x)
(x : α)
:
hwf.fix F x = F x fun (y : α) (x : r y x) => hwf.fix F y
Equations
- emptyWf = { rel := emptyRelation, wf := ⋯ }
theorem
Subrelation.accessible
{α : Sort u}
{r q : α → α → Prop}
{a : α}
(h₁ : Subrelation q r)
(ac : Acc r a)
:
Acc q a
theorem
Subrelation.wf
{α : Sort u}
{r q : α → α → Prop}
(h₁ : Subrelation q r)
(h₂ : WellFounded r)
:
theorem
InvImage.wf
{α : Sort u}
{β : Sort v}
{r : β → β → Prop}
(f : α → β)
(h : WellFounded r)
:
WellFounded (InvImage r f)
@[reducible]
theorem
Acc.transGen
{α✝ : Sort u_1}
{r : α✝ → α✝ → Prop}
{a : α✝}
(h : Acc r a)
:
Acc (Relation.TransGen r) a
theorem
acc_transGen_iff
{α✝ : Sort u_1}
{r : α✝ → α✝ → Prop}
{a : α✝}
:
Acc (Relation.TransGen r) a ↔ Acc r a
@[reducible, inline, deprecated Acc.transGen]
abbrev
TC.accessible
{α✝ : Sort u_1}
{r : α✝ → α✝ → Prop}
{a : α✝}
(h : Acc r a)
:
Acc (Relation.TransGen r) a
Equations
@[reducible, inline, deprecated WellFounded.transGen]
Equations
Equations
- Nat.lt_wfRel = { rel := fun (x1 x2 : Nat) => x1 < x2, wf := Nat.lt_wfRel.proof_1 }
noncomputable def
Nat.strongRecOn
{motive : Nat → Sort u}
(n : Nat)
(ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n)
:
motive n
Equations
- Nat.strongRecOn n ind = ⋯.fix ind n
@[deprecated Nat.strongRecOn]
noncomputable def
Nat.strongInductionOn
{motive : Nat → Sort u}
(n : Nat)
(ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n)
:
motive n
Equations
- Nat.strongInductionOn n ind = Nat.strongRecOn n ind
@[deprecated Nat.caseStrongRecOn]
noncomputable def
Nat.caseStrongInductionOn
{motive : Nat → Sort u}
(a : Nat)
(zero : motive 0)
(ind : (n : Nat) → ((m : Nat) → m ≤ n → motive m) → motive n.succ)
:
motive a
Equations
- Nat.caseStrongInductionOn a zero ind = Nat.caseStrongRecOn a zero ind
@[reducible, inline]
Equations
- measure f = invImage f Nat.lt_wfRel
@[reducible, inline]
@[instance 100]
Equations
- instWellFoundedRelationOfSizeOf = sizeOfWFRel
instance
Prod.Lex.instDecidableRelOfDecidableEq
{α : Type u}
{β : Type v}
[αeqDec : DecidableEq α]
{r : α → α → Prop}
[rDec : DecidableRel r]
{s : β → β → Prop}
[sDec : DecidableRel s]
:
DecidableRel (Prod.Lex r s)
Equations
- One or more equations did not get rendered due to their size.
@[reducible]
def
Prod.lex
{α : Type u}
{β : Type v}
(ha : WellFoundedRelation α)
(hb : WellFoundedRelation β)
:
WellFoundedRelation (α × β)
instance
Prod.instWellFoundedRelation
{α : Type u}
{β : Type v}
[ha : WellFoundedRelation α]
[hb : WellFoundedRelation β]
:
WellFoundedRelation (α × β)
theorem
Prod.RProdSubLex
{α : Type u}
{β : Type v}
{ra : α → α → Prop}
{rb : β → β → Prop}
(a b : α × β)
(h : Prod.RProd ra rb a b)
:
Prod.Lex ra rb a b
def
Prod.rprod
{α : Type u}
{β : Type v}
(ha : WellFoundedRelation α)
(hb : WellFoundedRelation β)
:
WellFoundedRelation (α × β)
Equations
- Prod.rprod ha hb = { rel := Prod.RProd WellFoundedRelation.rel WellFoundedRelation.rel, wf := ⋯ }
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
theorem
PSigma.lexAccessible
{α : Sort u}
{β : α → Sort v}
{r : α → α → Prop}
{s : (a : α) → β a → β a → Prop}
{a : α}
(aca : Acc r a)
(acb : ∀ (a : α), WellFounded (s a))
(b : β a)
:
Acc (PSigma.Lex r s) ⟨a, b⟩
@[reducible]
def
PSigma.lex
{α : Sort u}
{β : α → Sort v}
(ha : WellFoundedRelation α)
(hb : (a : α) → WellFoundedRelation (β a))
:
Equations
- PSigma.lex ha hb = { rel := PSigma.Lex WellFoundedRelation.rel fun (a : α) => WellFoundedRelation.rel, wf := ⋯ }
instance
PSigma.instWellFoundedRelation
{α : Sort u}
{β : α → Sort v}
[ha : WellFoundedRelation α]
[hb : (a : α) → WellFoundedRelation (β a)]
:
Equations
- PSigma.instWellFoundedRelation = PSigma.lex ha hb
def
PSigma.lexNdep
{α : Sort u}
{β : Sort v}
(r : α → α → Prop)
(s : β → β → Prop)
:
(_ : α) ×' β → (_ : α) ×' β → Prop
Equations
- PSigma.lexNdep r s = PSigma.Lex r fun (x : α) => s
theorem
PSigma.lexNdepWf
{α : Sort u}
{β : Sort v}
{r : α → α → Prop}
{s : β → β → Prop}
(ha : WellFounded r)
(hb : WellFounded s)
:
WellFounded (PSigma.lexNdep r s)
inductive
PSigma.RevLex
{α : Sort u}
{β : Sort v}
(r : α → α → Prop)
(s : β → β → Prop)
:
(_ : α) ×' β → (_ : α) ×' β → Prop
- left: ∀ {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} {a₁ a₂ : α} (b : β), r a₁ a₂ → PSigma.RevLex r s ⟨a₁, b⟩ ⟨a₂, b⟩
- right: ∀ {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β}, s b₁ b₂ → PSigma.RevLex r s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
theorem
PSigma.revLexAccessible
{α : Sort u}
{β : Sort v}
{r : α → α → Prop}
{s : β → β → Prop}
{b : β}
(acb : Acc s b)
(aca : ∀ (a : α), Acc r a)
(a : α)
:
Acc (PSigma.RevLex r s) ⟨a, b⟩
theorem
PSigma.revLex
{α : Sort u}
{β : Sort v}
{r : α → α → Prop}
{s : β → β → Prop}
(ha : WellFounded r)
(hb : WellFounded s)
:
WellFounded (PSigma.RevLex r s)
def
PSigma.SkipLeft
(α : Type u)
{β : Type v}
(s : β → β → Prop)
:
(_ : α) ×' β → (_ : α) ×' β → Prop
Equations
- PSigma.SkipLeft α s = PSigma.RevLex emptyRelation s
def
PSigma.skipLeft
(α : Type u)
{β : Type v}
(hb : WellFoundedRelation β)
:
WellFoundedRelation ((_ : α) ×' β)
Equations
- PSigma.skipLeft α hb = { rel := PSigma.SkipLeft α WellFoundedRelation.rel, wf := ⋯ }
theorem
PSigma.mkSkipLeft
{α : Type u}
{β : Type v}
{b₁ b₂ : β}
{s : β → β → Prop}
(a₁ a₂ : α)
(h : s b₁ b₂)
:
PSigma.SkipLeft α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩