Well-founded relations #

A relation is well-founded if it can be used for induction: for each x, (∀ y, r y x → P y) → P x implies P x. Well-founded relations can be used for induction and recursion, including construction of fixed points in the space of dependent functions Π x : α , β x.

The predicate well_founded is defined in the core library. In this file we prove some extra lemmas and provide a few new definitions: well_founded.min, well_founded.sup, and well_founded.succ.

source

theorem well_founded.has_min {α : Type u_1} {r : α → α → Prop} (H : well_founded r) (s : set α) :

s.nonempty → (∃ (a : α) (H : a ∈ s), ∀ (x : α), x ∈ s → ¬r x a)

If r is a well-founded relation, then any nonempty set has a minimal element with respect to r.

source

def well_founded.min {α : Type u_1} {r : α → α → Prop} (H : well_founded r) (p : set α) (h : p.nonempty) :

A minimal element of a nonempty set in a well-founded order

Equations

H.min p h = classical.some _

source

theorem well_founded.min_mem {α : Type u_1} {r : α → α → Prop} (H : well_founded r) (p : set α) (h : p.nonempty) :

H.min p h ∈ p

source

theorem well_founded.not_lt_min {α : Type u_1} {r : α → α → Prop} (H : well_founded r) (p : set α) (h : p.nonempty) {x : α} (xp : x ∈ p) :

¬r x (H.min p h)

source

theorem well_founded.well_founded_iff_has_min {α : Type u_1} {r : α → α → Prop} :

well_founded r ↔ ∀ (p : set α), p.nonempty → (∃ (m : α) (H : m ∈ p), ∀ (x : α), x ∈ p → ¬r x m)

source

theorem well_founded.eq_iff_not_lt_of_le {α : Type u_1} [partial_order α] {x y : α} :

x ≤ y → y = x ↔ ¬x < y

source

theorem well_founded.well_founded_iff_has_max' {α : Type u_1} [partial_order α] :

well_founded gt ↔ ∀ (p : set α), p.nonempty → (∃ (m : α) (H : m ∈ p), ∀ (x : α), x ∈ p → m ≤ x → x = m)

source

theorem well_founded.well_founded_iff_has_min' {α : Type u_1} [partial_order α] :

well_founded has_lt.lt ↔ ∀ (p : set α), p.nonempty → (∃ (m : α) (H : m ∈ p), ∀ (x : α), x ∈ p → x ≤ m → x = m)

source

def well_founded.sup {α : Type u_1} {r : α → α → Prop} (wf : well_founded r) (s : set α) (h : bounded r s) :

The supremum of a bounded, well-founded order

Equations

wf.sup s h = wf.min {x : α | ∀ (a : α), a ∈ s → r a x} h

source

theorem well_founded.lt_sup {α : Type u_1} {r : α → α → Prop} (wf : well_founded r) {s : set α} (h : bounded r s) {x : α} (hx : x ∈ s) :

r x (wf.sup s h)

source

def well_founded.succ {α : Type u_1} {r : α → α → Prop} (wf : well_founded r) (x : α) :

A successor of an element x in a well-founded order is a minimal element y such that x < y if one exists. Otherwise it is x itself.

Equations

wf.succ x = dite (∃ (y : α), r x y) (λ (h : ∃ (y : α), r x y), wf.min {y : α | r x y} h) (λ (h : ¬∃ (y : α), r x y), x)

source

theorem well_founded.lt_succ {α : Type u_1} {r : α → α → Prop} (wf : well_founded r) {x : α} (h : ∃ (y : α), r x y) :

r x (wf.succ x)

source

theorem well_founded.lt_succ_iff {α : Type u_1} {r : α → α → Prop} [wo : is_well_order α r] {x : α} (h : ∃ (y : α), r x y) (y : α) :

r y (is_well_order.wf.succ x) ↔ r y x ∨ y = x