# 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 `WellFounded` is defined in the core library. In this file we prove some extra lemmas and provide a few new definitions: `WellFounded.min`, `WellFounded.sup`, and `WellFounded.succ`, and an induction principle `WellFounded.induction_bot`.

source
theorem acc_def {α : Sort u_1} {r : α → α → Prop} {a : α} :
Acc r a ↔ ∀ (b : α), r b a → Acc r b
source
theorem exists_not_acc_lt_of_not_acc {α : Sort u_1} {a : α} {r : α → α → Prop} (h : ¬Acc r a) :
∃ (b : α), ¬Acc r b ∧ r b a
source
theorem not_acc_iff_exists_descending_chain {α : Sort u_1} {r : α → α → Prop} {x : α} :
¬Acc r x ↔ ∃ (f : ℕ → α), f 0 = x ∧ ∀ (n : ℕ), r (f (n + 1)) (f n)
source
theorem acc_iff_isEmpty_descending_chain {α : Sort u_1} {r : α → α → Prop} {x : α} :
Acc r x ↔ IsEmpty { f : ℕ → α // f 0 = x ∧ ∀ (n : ℕ), r (f (n + 1)) (f n) }
source
theorem wellFounded_iff_isEmpty_descending_chain {α : Sort u_1} {r : α → α → Prop} :
WellFounded r ↔ IsEmpty { f : ℕ → α // ∀ (n : ℕ), r (f (n + 1)) (f n) }

A relation is well-founded iff it doesn't have any infinite descending chain.

See `RelEmbedding.wellFounded_iff_isEmpty` for a version in terms of relation embeddings.

source
theorem WellFounded.isAsymm {α : Type u_1} {r : α → α → Prop} (h : WellFounded r) :
IsAsymm α r
source
theorem WellFounded.isIrrefl {α : Type u_1} {r : α → α → Prop} (h : WellFounded r) :
IsIrrefl α r
source
instance WellFounded.instIsAsymmRel {α : Type u_1} [WellFoundedRelation α] :
IsAsymm α WellFoundedRelation.rel
source
instance WellFounded.instIsIrreflRel {α : Type u_1} :
IsIrrefl α WellFoundedRelation.rel
source
theorem WellFounded.mono {α : Type u_1} {r r' : α → α → Prop} (hr : WellFounded r) (h : ∀ (a b : α), r' a b → r a b) :
WellFounded r'
source
theorem WellFounded.onFun {α : Sort u_4} {β : Sort u_5} {r : β → β → Prop} {f : α → β} :
WellFounded r → WellFounded (Function.onFun r f)
source
theorem WellFounded.has_min {α : Type u_4} {r : α → α → Prop} (H : WellFounded r) (s : Set α) :
s.Nonempty → ∃ a ∈ s, ∀ 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
noncomputable def WellFounded.min {α : Type u_1} {r : α → α → Prop} (H : WellFounded 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 `ConditionallyCompleteLinearOrderBot` instance via `WellFoundedLT.conditionallyCompleteLinearOrderBot` and using `Inf` instead.

Equations

- H.min s h = Classical.choose ⋯

Instances For

source
theorem WellFounded.min_mem {α : Type u_1} {r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : s.Nonempty) :
H.min s h ∈ s
source
theorem WellFounded.not_lt_min {α : Type u_1} {r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : s.Nonempty) {x : α} (hx : x ∈ s) :
¬r x (H.min s h)
source
theorem WellFounded.wellFounded_iff_has_min {α : Type u_1} {r : α → α → Prop} :
WellFounded r ↔ ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
source
@[deprecated wellFounded_iff_isEmpty_descending_chain (since := "2025-08-10")]
theorem WellFounded.wellFounded_iff_no_descending_seq {α : Sort u_1} {r : α → α → Prop} :
WellFounded r ↔ IsEmpty { f : ℕ → α // ∀ (n : ℕ), r (f (n + 1)) (f n) }

Alias of `wellFounded_iff_isEmpty_descending_chain`.

A relation is well-founded iff it doesn't have any infinite descending chain.

See `RelEmbedding.wellFounded_iff_isEmpty` for a version in terms of relation embeddings.

source
theorem WellFounded.not_rel_apply_succ {α : Type u_1} {r : α → α → Prop} [h : IsWellFounded α r] (f : ℕ → α) :
∃ (n : ℕ), ¬r (f (n + 1)) (f n)
source
noncomputable def WellFounded.sup {α : Type u_1} {r : α → α → Prop} (wf : WellFounded 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 ∈ s, r a x} h

Instances For

source
theorem WellFounded.lt_sup {α : Type u_1} {r : α → α → Prop} (wf : WellFounded r) {s : Set α} (h : Set.Bounded r s) {x : α} (hx : x ∈ s) :
r x (wf.sup s h)
source
theorem WellFounded.min_le {β : Type u_2} [LinearOrder β] (h : WellFounded fun (x1 x2 : β) => x1 < x2) {x : β} {s : Set β} (hx : x ∈ s) (hne : s.Nonempty := ⋯) :
h.min s hne ≤ x
source
theorem Set.range_injOn_strictMono {β : Type u_2} {γ : Type u_3} [LinearOrder β] [Preorder γ] [WellFoundedLT β] :
InjOn range {f : β → γ | StrictMono f}
source
theorem Set.range_injOn_strictAnti {β : Type u_2} {γ : Type u_3} [LinearOrder β] [Preorder γ] [WellFoundedGT β] :
InjOn range {f : β → γ | StrictAnti f}
source
theorem StrictMono.range_inj {β : Type u_2} {γ : Type u_3} [LinearOrder β] [Preorder γ] [WellFoundedLT β] {f g : β → γ} (hf : StrictMono f) (hg : StrictMono g) :
Set.range f = Set.range g ↔ f = g
source
theorem StrictAnti.range_inj {β : Type u_2} {γ : Type u_3} [LinearOrder β] [Preorder γ] [WellFoundedGT β] {f g : β → γ} (hf : StrictAnti f) (hg : StrictAnti g) :
Set.range f = Set.range g ↔ f = g
source
theorem StrictMono.id_le {β : Type u_2} [LinearOrder β] [WellFoundedLT β] {f : β → β} (hf : StrictMono f) :
id ≤ f

A strictly monotone function `f` on a well-order satisfies `x ≤ f x` for all `x`.

source
theorem StrictMono.le_apply {β : Type u_2} [LinearOrder β] [WellFoundedLT β] {f : β → β} (hf : StrictMono f) {x : β} :
x ≤ f x
source
theorem StrictMono.le_id {β : Type u_2} [LinearOrder β] [WellFoundedGT β] {f : β → β} (hf : StrictMono f) :
f ≤ id

A strictly monotone function `f` on a cowell-order satisfies `f x ≤ x` for all `x`.

source
theorem StrictMono.apply_le {β : Type u_2} [LinearOrder β] [WellFoundedGT β] {f : β → β} (hf : StrictMono f) {x : β} :
f x ≤ x
source
theorem StrictMono.not_bddAbove_range_of_wellFoundedLT {β : Type u_2} [LinearOrder β] {f : β → β} [WellFoundedLT β] [NoMaxOrder β] (hf : StrictMono f) :
¬BddAbove (Set.range f)
source
theorem StrictMono.not_bddBelow_range_of_wellFoundedGT {β : Type u_2} [LinearOrder β] {f : β → β} [WellFoundedGT β] [NoMinOrder β] (hf : StrictMono f) :
¬BddBelow (Set.range f)
source
noncomputable def Function.argmin {α : Type u_1} {β : Type u_2} (f : α → β) [LT β] [h : WellFoundedLT β] [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 = ⋯.min Set.univ ⋯

Instances For

source
theorem Function.not_lt_argmin {α : Type u_1} {β : Type u_2} (f : α → β) [LT β] [h : WellFoundedLT β] [Nonempty α] (a : α) :
¬f a < f (argmin f)
source
noncomputable def Function.argminOn {α : Type u_1} {β : Type u_2} (f : α → β) [LT β] [h : WellFoundedLT β] (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_argminOn`.

Equations

- Function.argminOn f s hs = ⋯.min s hs

Instances For

source
@[simp]
theorem Function.argminOn_mem {α : Type u_1} {β : Type u_2} (f : α → β) [LT β] [h : WellFoundedLT β] (s : Set α) (hs : s.Nonempty) :
argminOn f s hs ∈ s
source
theorem Function.not_lt_argminOn {α : Type u_1} {β : Type u_2} (f : α → β) [LT β] [h : WellFoundedLT β] (s : Set α) {a : α} (ha : a ∈ s) (hs : s.Nonempty := ⋯) :
¬f a < f (argminOn f s hs)
source
theorem Function.argmin_le {α : Type u_1} {β : Type u_2} (f : α → β) [LinearOrder β] [WellFoundedLT β] (a : α) [Nonempty α] :
f (argmin f) ≤ f a
source
theorem Function.argminOn_le {α : Type u_1} {β : Type u_2} (f : α → β) [LinearOrder β] [WellFoundedLT β] (s : Set α) {a : α} (ha : a ∈ s) (hs : s.Nonempty := ⋯) :
f (argminOn f s hs) ≤ f a
source
theorem Acc.induction_bot' {α : Sort u_4} {β : Sort u_5} {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)`.

source
theorem Acc.induction_bot {α : Sort u_4} {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`.

source
theorem WellFounded.induction_bot' {α : Sort u_4} {β : Sort u_5} {r : α → α → Prop} (hwf : WellFounded 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)`.

source
theorem WellFounded.induction_bot {α : Sort u_4} {r : α → α → Prop} (hwf : WellFounded 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`.

source
noncomputable def WellFoundedLT.toOrderBot {α : Type u_4} [LinearOrder α] [Nonempty α] [h : WellFoundedLT α] :
OrderBot α

A nonempty linear order with well-founded `<` has a bottom element.

Equations

- WellFoundedLT.toOrderBot = { bot := ⋯.min Set.univ ⋯, bot_le := ⋯ }

Instances For

source
noncomputable def WellFoundedGT.toOrderTop {α : Type u_4} [LinearOrder α] [Nonempty α] [WellFoundedGT α] :
OrderTop α

A nonempty linear order with well-founded `>` has a top element.

Equations

- WellFoundedGT.toOrderTop = inferInstanceAs (OrderTop α ᵒᵈ ᵒᵈ)

Instances For

source
instance ULift.instWellFoundedLT {α : Type u_1} [LT α] [h : WellFoundedLT α] :
WellFoundedLT (ULift.{u_4, u_1} α)
source
instance ULift.instWellFoundedGT {α : Type u_1} [LT α] [WellFoundedGT α] :
WellFoundedGT (ULift.{u_4, u_1} α)