- intro: ∀ {α : Sort u} {r : α → α → Prop}, (∀ (a : α), Acc r a) → WellFounded r
Instances For
- rel : α → α → Prop
- wf : WellFounded WellFoundedRelation.rel
Instances
Instances For
theorem
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
def
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 => WellFounded.fixF F y (_ : Acc (fun y x => r y x) y)
Instances For
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
Instances For
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 : α)
:
WellFounded.fix hwf F x = F x fun y x => WellFounded.fix hwf F y
def
Subrelation.accessible
{α : Sort u}
{r : α → α → Prop}
{q : α → α → Prop}
{a : α}
(h₁ : Subrelation q r)
(ac : Acc r a)
:
Acc q a
Instances For
def
Subrelation.wf
{α : Sort u}
{r : α → α → Prop}
{q : α → α → Prop}
(h₁ : Subrelation q r)
(h₂ : WellFounded r)
:
Instances For
def
InvImage.wf
{α : Sort u}
{β : Sort v}
{r : β → β → Prop}
(f : α → β)
(h : WellFounded r)
:
WellFounded (InvImage r f)
Instances For
@[reducible]
Instances For
Instances For
@[inline, reducible]
Instances For
@[inline, reducible]
Instances For
- left: ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} {a₁ : α} (b₁ : β) {a₂ : α} (b₂ : β), ra a₁ a₂ → Prod.Lex ra rb (a₁, b₁) (a₂, b₂)
- right: ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (a : α) {b₁ b₂ : β}, rb b₁ b₂ → Prod.Lex ra rb (a, b₁) (a, b₂)
Instances For
@[reducible]
def
Prod.lex
{α : Type u}
{β : Type v}
(ha : WellFoundedRelation α)
(hb : WellFoundedRelation β)
:
WellFoundedRelation (α × β)
Instances For
instance
Prod.instWellFoundedRelationProd
{α : Type u}
{β : Type v}
[ha : WellFoundedRelation α]
[hb : WellFoundedRelation β]
:
WellFoundedRelation (α × β)
def
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
Instances For
def
Prod.rprod
{α : Type u}
{β : Type v}
(ha : WellFoundedRelation α)
(hb : WellFoundedRelation β)
:
WellFoundedRelation (α × β)
Instances For
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 { fst := a₁, snd := b₁ } { fst := a₂, snd := 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 { fst := a, snd := b₁ } { fst := a, snd := b₂ }
Instances For
def
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) { fst := a, snd := b }
Instances For
@[reducible]
def
PSigma.lex
{α : Sort u}
{β : α → Sort v}
(ha : WellFoundedRelation α)
(hb : (a : α) → WellFoundedRelation (β a))
:
Instances For
instance
PSigma.instWellFoundedRelationPSigma
{α : Sort u}
{β : α → Sort v}
[ha : WellFoundedRelation α]
[hb : (a : α) → WellFoundedRelation (β a)]
:
def
PSigma.lexNdepWf
{α : Sort u}
{β : Sort v}
{r : α → α → Prop}
{s : β → β → Prop}
(ha : WellFounded r)
(hb : WellFounded s)
:
WellFounded (PSigma.lexNdep r s)
Instances For
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 { fst := a₁, snd := b } { fst := a₂, snd := b }
- right: ∀ {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β}, s b₁ b₂ → PSigma.RevLex r s { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }
Instances For
def
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) { fst := a, snd := b }
Instances For
def
PSigma.revLex
{α : Sort u}
{β : Sort v}
{r : α → α → Prop}
{s : β → β → Prop}
(ha : WellFounded r)
(hb : WellFounded s)
:
WellFounded (PSigma.RevLex r s)
Instances For
def
PSigma.skipLeft
(α : Type u)
{β : Type v}
(hb : WellFoundedRelation β)
:
WellFoundedRelation ((_ : α) ×' β)
Instances For
def
PSigma.mkSkipLeft
{α : Type u}
{β : Type v}
{b₁ : β}
{b₂ : β}
{s : β → β → Prop}
(a₁ : α)
(a₂ : α)
(h : s b₁ b₂)
:
PSigma.SkipLeft α s { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }