# mathlibdocumentation

order.well_founded

# 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.

@[protected]
theorem well_founded.is_asymm {α : Type u_1} {r : α → α → Prop} (h : well_founded r) :
r
@[protected, instance]
@[protected]
theorem well_founded.is_irrefl {α : Type u_1} {r : α → α → Prop} (h : well_founded r) :
r
@[protected, instance]
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
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} :
∀ (s : set α), s.nonempty(∃ (m : α) (H : m s), ∀ (x : α), x s¬r x m)
theorem well_founded.eq_iff_not_lt_of_le {α : Type u_1} {x y : α} :
x yy = x ¬x < y
theorem well_founded.well_founded_iff_has_max' {α : Type u_1}  :
∀ (p : set α), p.nonempty(∃ (m : α) (H : m p), ∀ (x : α), x pm xx = m)
theorem well_founded.well_founded_iff_has_min' {α : Type u_1}  :
∀ (p : set α), p.nonempty(∃ (m : α) (H : m p), ∀ (x : α), x px mx = m)
@[protected]
noncomputable def well_founded.sup {α : Type u_1} {r : α → α → Prop} (wf : well_founded r) (s : set α) (h : s) :
α

The supremum of a bounded, well-founded order

Equations
• wf.sup s h = wf.min {x : α | ∀ (a : α), a sr a x} h
@[protected]
theorem well_founded.lt_sup {α : Type u_1} {r : α → α → Prop} (wf : well_founded r) {s : set α} (h : 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 : r] {x : α} (h : ∃ (y : α), r x y) (y : α) :
r y r y x y = x
theorem well_founded.min_le {β : Type u_2} [linear_order β] {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} [linear_order β] {γ : Type u_3} {f g : β → γ} (hf : strict_mono f) (hg : strict_mono g) :
f = g
theorem well_founded.self_le_of_strict_mono {β : Type u_2} [linear_order β] {f : β → β} (hf : strict_mono f) (n : β) :
n f n
noncomputable def function.argmin {α : Type u_1} {β : Type u_2} (f : α → β) [has_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
theorem function.not_lt_argmin {α : Type u_1} {β : Type u_2} (f : α → β) [has_lt β] [nonempty α] (a : α) :
¬f a < f h)
noncomputable def function.argmin_on {α : Type u_1} {β : Type u_2} (f : α → β) [has_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
@[simp]
theorem function.argmin_on_mem {α : Type u_1} {β : Type u_2} (f : α → β) [has_lt β] (s : set α) (hs : s.nonempty) :
s hs s
@[simp]
theorem function.not_lt_argmin_on {α : Type u_1} {β : Type u_2} (f : α → β) [has_lt β] (s : set α) {a : α} (ha : a s) (hs : s.nonempty := _) :
¬f a < f s hs)
@[simp]
theorem function.argmin_le {α : Type u_1} {β : Type u_2} (f : α → β) [linear_order β] (a : α) [nonempty α] :
f h) f a
@[simp]
theorem function.argmin_on_le {α : Type u_1} {β : Type u_2} (f : α → β) [linear_order β] (s : set α) {a : α} (ha : a s) (hs : s.nonempty := _) :
f s hs) f a