mathlib3 documentation

order.well_founded

Well-founded relations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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, and an induction principle well_founded.induction_bot.

@[protected]

theorem well_founded.is_asymm {α : Type u_1} {r : α → α → Prop} (h : well_founded r) :

@[protected]

theorem well_founded.is_irrefl {α : Type u_1} {r : α → α → Prop} (h : well_founded r) :

@[protected, instance]

def well_founded.has_well_founded.r.is_asymm {α : Type u_1} [has_well_founded α] :

is_asymm α has_well_founded.r

@[protected, instance]

def well_founded.has_well_founded.r.is_irrefl {α : Type u_1} [has_well_founded α] :

is_irrefl α has_well_founded.r

theorem well_founded.mono {α : Type u_1} {r r' : α → α → Prop} (hr : well_founded r) (h : ∀ (a b : α), r' a b → r a b) :

well_founded r'

theorem well_founded.on_fun {α : Sort u_1} {β : Sort u_2} {r : β → β → Prop} {f : α → β} :

well_founded r → well_founded (r on f)

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.

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

α

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

If you're working with a nonempty linear order, consider defining a conditionally_complete_linear_order_bot instance via well_founded.conditionally_complete_linear_order_with_bot and using Inf instead.

Equations

H.min s h = classical.some _

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

H.min s h ∈ s

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

¬r x (H.min s h)

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

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

@[protected]

noncomputable def well_founded.sup {α : Type u_1} {r : α → α → Prop} (wf : well_founded r) (s : set α) (h : set.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

@[protected]

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

r x (wf.sup s h)

@[protected]

noncomputable 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)

@[protected]

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)

@[protected]

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_founded.wf.succ x) ↔ r y x ∨ y = x

theorem well_founded.min_le {β : Type u_2} [linear_order β] (h : well_founded has_lt.lt) {x : β} {s : set β} (hx : x ∈ s) (hne : s.nonempty := _) :

h.min s hne ≤ x

theorem well_founded.eq_strict_mono_iff_eq_range {β : Type u_2} {γ : Type u_3} [linear_order β] (h : well_founded has_lt.lt) [partial_order γ] {f g : β → γ} (hf : strict_mono f) (hg : strict_mono g) :

set.range f = set.range g ↔ f = g

theorem well_founded.self_le_of_strict_mono {β : Type u_2} [linear_order β] (h : well_founded has_lt.lt) {f : β → β} (hf : strict_mono f) (n : β) :

n ≤ f n

noncomputable def function.argmin {α : Type u_1} {β : Type u_2} (f : α → β) [has_lt β] (h : well_founded has_lt.lt) [nonempty α] :

α

Given a function f : α → β where β carries a well-founded <, this is an element of α whose image under f is minimal in the sense of function.not_lt_argmin.

Equations

function.argmin f h = _.min set.univ set.univ_nonempty

theorem function.not_lt_argmin {α : Type u_1} {β : Type u_2} (f : α → β) [has_lt β] (h : well_founded has_lt.lt) [nonempty α] (a : α) :

¬f a < f (function.argmin f h)

noncomputable def function.argmin_on {α : Type u_1} {β : Type u_2} (f : α → β) [has_lt β] (h : well_founded has_lt.lt) (s : set α) (hs : s.nonempty) :

α

Given a function f : α → β where β carries a well-founded <, and a non-empty subset s of α, this is an element of s whose image under f is minimal in the sense of function.not_lt_argmin_on.

Equations

function.argmin_on f h s hs = _.min s hs

@[simp]

theorem function.argmin_on_mem {α : Type u_1} {β : Type u_2} (f : α → β) [has_lt β] (h : well_founded has_lt.lt) (s : set α) (hs : s.nonempty) :

function.argmin_on f h s hs ∈ s

@[simp]

theorem function.not_lt_argmin_on {α : Type u_1} {β : Type u_2} (f : α → β) [has_lt β] (h : well_founded has_lt.lt) (s : set α) {a : α} (ha : a ∈ s) (hs : s.nonempty := _) :

¬f a < f (function.argmin_on f h s hs)

@[simp]

theorem function.argmin_le {α : Type u_1} {β : Type u_2} (f : α → β) [linear_order β] (h : well_founded has_lt.lt) (a : α) [nonempty α] :

f (function.argmin f h) ≤ f a

@[simp]

theorem function.argmin_on_le {α : Type u_1} {β : Type u_2} (f : α → β) [linear_order β] (h : well_founded has_lt.lt) (s : set α) {a : α} (ha : a ∈ s) (hs : s.nonempty := _) :

f (function.argmin_on f h s hs) ≤ f a

theorem acc.induction_bot' {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} {a bot : α} (ha : acc r a) {C : β → Prop} {f : α → β} (ih : ∀ (b : α), f b ≠ f bot → C (f b) → (∃ (c : α), r c b ∧ C (f c))) :

C (f a) → C (f bot)

Let r be a relation on α, let f : α → β be a function, let C : β → Prop, and let bot : α. This induction principle shows that C (f bot) holds, given that

some a that is accessible by r satisfies C (f a), and
for each b such that f b ≠ f bot and C (f b) holds, there is c satisfying r c b and C (f c).

theorem acc.induction_bot {α : Sort u_1} {r : α → α → Prop} {a bot : α} (ha : acc r a) {C : α → Prop} (ih : ∀ (b : α), b ≠ bot → C b → (∃ (c : α), r c b ∧ C c)) :

C a → C bot

Let r be a relation on α, let C : α → Prop and let bot : α. This induction principle shows that C bot holds, given that

some a that is accessible by r satisfies C a, and
for each b ≠ bot such that C b holds, there is c satisfying r c b and C c.

theorem well_founded.induction_bot' {α : Sort u_1} {β : Sort u_2} {r : α → α → Prop} (hwf : well_founded r) {a bot : α} {C : β → Prop} {f : α → β} (ih : ∀ (b : α), f b ≠ f bot → C (f b) → (∃ (c : α), r c b ∧ C (f c))) :

C (f a) → C (f bot)

Let r be a well-founded relation on α, let f : α → β be a function, let C : β → Prop, and let bot : α. This induction principle shows that C (f bot) holds, given that

some a satisfies C (f a), and
for each b such that f b ≠ f bot and C (f b) holds, there is c satisfying r c b and C (f c).

theorem well_founded.induction_bot {α : Sort u_1} {r : α → α → Prop} (hwf : well_founded r) {a bot : α} {C : α → Prop} (ih : ∀ (b : α), b ≠ bot → C b → (∃ (c : α), r c b ∧ C c)) :

C a → C bot

Let r be a well-founded relation on α, let C : α → Prop, and let bot : α. This induction principle shows that C bot holds, given that

some a satisfies C a, and
for each b that satisfies C b, there is c satisfying r c b and C c.

The naming is inspired by the fact that when r is transitive, it follows that bot is the smallest element w.r.t. r that satisfies C.