mathlib documentation

core.init.wf

inductive acc {α : Sort u} :
(α → α → Prop)α → Prop
  • intro : ∀ {α : Sort u} (r : α → α → Prop) (x : α), (∀ (y : α), r y xacc r y)acc r x

def acc.inv {α : Sort u} {r : α → α → Prop} {x y : α} :
acc r xr y xacc r y

structure well_founded {α : Sort u} :
(α → α → Prop) → Prop
  • apply : ∀ (a : α), acc r a

A relation r : α → α → Prop is well-founded when ∀ x, (∀ y, r y x → P y → P x) → P x for all predicates P. Once you know that a relation is well_founded, you can use it to define fixpoint functions on α.

theorem well_founded.recursion {α : Sort u} {r : α → α → Prop} (hwf : well_founded r) {C : α → Sort v} (a : α) :
(Π (x : α), (Π (y : α), r y xC y)C x)C a

theorem well_founded.induction {α : Sort u} {r : α → α → Prop} (hwf : well_founded r) {C : α → Prop} (a : α) :
(∀ (x : α), (∀ (y : α), r y xC y)C x)C a

def well_founded.fix_F {α : Sort u} {r : α → α → Prop} {C : α → Sort v} (F : Π (x : α), (Π (y : α), r y xC y)C x) (x : α) :
acc r xC x

Equations
  • well_founded.fix_F F x a = a.rec_on (λ (x₁ : α) (ac₁ : ∀ (y : α), r y x₁acc r y) (ih : Π (y : α), r y x₁C y), F x₁ ih)
theorem well_founded.fix_F_eq {α : Sort u} {r : α → α → Prop} {C : α → Sort v} (F : Π (x : α), (Π (y : α), r y xC y)C x) (x : α) (acx : acc r x) :
well_founded.fix_F F x acx = F x (λ (y : α) (p : r y x), well_founded.fix_F F y _)

def well_founded.fix {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : well_founded r) (F : Π (x : α), (Π (y : α), r y xC y)C x) (x : α) :
C x

Well-founded fixpoint

Equations
theorem well_founded.fix_eq {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : well_founded r) (F : Π (x : α), (Π (y : α), r y xC y)C x) (x : α) :
hwf.fix F x = F x (λ (y : α) (h : r y x), hwf.fix F y)

Well-founded fixpoint satisfies fixpoint equation

def empty_wf {α : Sort u} :

Empty relation is well-founded

def subrelation.accessible {α : Sort u} {r Q : α → α → Prop} (h₁ : subrelation Q r) {a : α} :
acc r aacc Q a

def subrelation.wf {α : Sort u} {r Q : α → α → Prop} :

def inv_image.accessible {α : Sort u} {β : Sort v} {r : β → β → Prop} (f : α → β) {a : α} :
acc r (f a)acc (inv_image r f) a

def inv_image.wf {α : Sort u} {β : Sort v} {r : β → β → Prop} (f : α → β) :

def tc.accessible {α : Sort u} {r : α → α → Prop} {z : α} :
acc r zacc (tc r) z

def tc.wf {α : Sort u} {r : α → α → Prop} :

less-than is well-founded

def measure {α : Sort u} :
(α → )α → α → Prop

Equations
def measure_wf {α : Sort u} (f : α → ) :

def sizeof_measure (α : Sort u) [has_sizeof α] :
α → α → Prop

Equations
@[instance]

Equations
inductive prod.lex {α : Type u} {β : Type v} :
(α → α → Prop)(β → β → Prop)α × βα × β → Prop
  • 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₂)

inductive prod.rprod {α : Type u} {β : Type v} :
(α → α → Prop)(β → β → Prop)α × βα × β → Prop
  • intro : ∀ {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → Prop) {a₁ : α} {b₁ : β} {a₂ : α} {b₂ : β}, ra a₁ a₂rb b₁ b₂prod.rprod ra rb (a₁, b₁) (a₂, b₂)

def prod.lex_accessible {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} {a : α} (aca : acc ra a) (acb : ∀ (b : β), acc rb b) (b : β) :
acc (prod.lex ra rb) (a, b)

def prod.lex_wf {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} :

def prod.rprod_sub_lex {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (a b : α × β) :
prod.rprod ra rb a bprod.lex ra rb a b

def prod.rprod_wf {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} :

@[instance]
def prod.has_well_founded {α : Type u} {β : Type v} [s₁ : has_well_founded α] [s₂ : has_well_founded β] :

Equations