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.

theorem acc_def {α : Sort u_1} {r : α → α → Prop} {a : α} : Acc r a ↔ ∀ (b : α), r b a → Acc r b

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

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)

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

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.

theorem WellFounded.asymm {α : Type u_1} {r : α → α → Prop} (h : WellFounded r) : Std.Asymm r

theorem WellFounded.irrefl {α : Type u_1} {r : α → α → Prop} (h : WellFounded r) : Std.Irrefl r

instance WellFounded.instAsymmRel_mathlib {α : Type u_1} [WellFoundedRelation α] : Std.Asymm WellFoundedRelation.rel

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

theorem WellFounded.onFun {α : Sort u_4} {β : Sort u_5} {r : β → β → Prop} {f : α → β} : WellFounded r → WellFounded (Function.onFun r f)

instance WellFounded.instIsWellFoundedOnFun {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α → β) [IsWellFounded β r] : IsWellFounded α (Function.onFun r f)

theorem Function.Injective.isWellOrder {α : Type u_1} {β : Type u_2} (r : β → β → Prop) {f : α → β} (hf : Injective f) [IsWellOrder β r] : IsWellOrder α (onFun r f)

theorem WellFounded.has_min {α : Type u_4} {r : α → α → Prop} (H : WellFounded r) (s : Set α) : s.Nonempty → ∃ (a : α), 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.

theorem WellFounded.not_rightTotal {α : Type u_1} {r : α → α → Prop} (wf : WellFounded r) [Nonempty α] : ¬Relator.RightTotal r

theorem WellFounded.not_leftTotal {α : Type u_1} {r : α → α → Prop} (wf : WellFounded (Function.swap r)) [Nonempty α] : ¬Relator.LeftTotal r

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 ⋯

@[reducible, inline]

noncomputable abbrev WellFoundedLT.min {α : Type u_1} [LT α] [WellFoundedLT α] (s : Set α) (h : s.Nonempty) : α

A minimal element of a nonempty set of a type with a well-founded <.

Equations

• WellFoundedLT.min s h = ⋯.min s h

@[reducible, inline]

noncomputable abbrev WellFoundedGT.max {α : Type u_1} [LT α] [WellFoundedGT α] (s : Set α) (h : s.Nonempty) : α

A maximal element of a nonempty set of a type with a well-founded >.

Equations

• WellFoundedGT.max s h = ⋯.min s h

theorem WellFounded.min_mem {α : Type u_1} {r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : s.Nonempty) : H.min s h ∈ s

theorem WellFounded.prop_min {α : Type u_1} {r : α → α → Prop} (H : WellFounded r) {p : α → Prop} (h : ∃ (a : α), p a) : p (H.min {a : α | p a} h)

theorem WellFounded.not_lt_min {α : Type u_1} {r : α → α → Prop} (H : WellFounded r) (s : Set α) {x : α} (hx : x ∈ s) : ¬r x (H.min s ⋯)

theorem WellFounded.min_eq_of_forall_not_lt {α : Type u_1} {r : α → α → Prop} [Std.Trichotomous r] (wf : WellFounded r) {s : Set α} {m : α} (hms : m ∈ s) (hrm : ∀ (x : α), x ∈ s → ¬r x m) : wf.min s ⋯ = m

The minimal element of a trichotomous well-founded order is unique

theorem WellFounded.notMem_of_lt_min {α : Type u_1} {r : α → α → Prop} {wf : WellFounded r} {s : Set α} {hs : s.Nonempty} {x : α} (hx : r x (wf.min s hs)) : ¬x ∈ s

theorem WellFounded.mem_of_lt_min_compl {α : Type u_1} {r : α → α → Prop} {wf : WellFounded r} {s : Set α} {hs : sᶜ.Nonempty} {x : α} (hx : r x (wf.min sᶜ hs)) : x ∈ s

theorem WellFounded.wellFounded_iff_has_min {α : Type u_1} {r : α → α → Prop} : WellFounded r ↔ ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m

theorem WellFounded.wellFoundedLT_iff_exists_minimal {α : Type u_1} [Preorder α] : WellFoundedLT α ↔ ∀ (s : Set α), s.Nonempty → ∃ (m : α), Minimal (fun (x : α) => x ∈ s) m

theorem WellFounded.wellFoundedGT_iff_exists_maximal {α : Type u_1} [Preorder α] : WellFoundedGT α ↔ ∀ (s : Set α), s.Nonempty → ∃ (m : α), Maximal (fun (x : α) => x ∈ s) m

theorem WellFoundedLT.exists_minimal {α : Type u_1} [Preorder α] : WellFoundedLT α → ∀ (s : Set α), s.Nonempty → ∃ (m : α), Minimal (fun (x : α) => x ∈ s) m

Alias of the forward direction of WellFounded.wellFoundedLT_iff_exists_minimal.

theorem WellFoundedGT.exists_maximal {α : Type u_1} [Preorder α] : WellFoundedGT α → ∀ (s : Set α), s.Nonempty → ∃ (m : α), Maximal (fun (x : α) => x ∈ s) m

Alias of the forward direction of WellFounded.wellFoundedGT_iff_exists_maximal.

theorem WellFounded.minimal_wellFounded_lt_min {α : Type u_1} [Preorder α] [WellFoundedLT α] {s : Set α} (h : s.Nonempty) : Minimal (fun (x : α) => x ∈ s) (⋯.min s h)

theorem WellFounded.maximal_wellFounded_lt_max {α : Type u_1} [Preorder α] [WellFoundedGT α] {s : Set α} (h : s.Nonempty) : Maximal (fun (x : α) => x ∈ s) (⋯.min s h)

theorem WellFounded.isWellOrder_iff_exists_not_lt_and_eq_or_gt {α : Type u_1} {r : α → α → Prop} : IsWellOrder α r ↔ ∀ (s : Set α), s.Nonempty → ∃ (m : α), m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)

theorem WellFounded.min_image {α : Type u_1} {β : Type u_2} {r : β → β → Prop} [Std.Trichotomous r] (wf : WellFounded r) (f : α → β) {s : Set α} (hne : s.Nonempty) : wf.min (f '' s) ⋯ = f (⋯.min s hne)

The minimum of f '' s is f applied to the minimum of s.

theorem WellFounded.not_rel_apply_succ {α : Type u_1} {r : α → α → Prop} [h : IsWellFounded α r] (f : ℕ → α) : ∃ (n : ℕ), ¬r (f (n + 1)) (f n)

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 : α), a ∈ s → r a x} h

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)

theorem WellFoundedLT.min_le {β : Type u_2} [LinearOrder β] [WellFoundedLT β] {x : β} {s : Set β} (hx : x ∈ s) : min s ⋯ ≤ x

theorem WellFoundedGT.le_max {β : Type u_2} [LinearOrder β] [WellFoundedGT β] {x : β} {s : Set β} (hx : x ∈ s) : x ≤ max s ⋯

@[deprecated WellFoundedLT.min_le (since := "2026-08-16")]

theorem WellFounded.min_le {β : Type u_2} [LinearOrder β] (h : WellFounded fun (x1 x2 : β) => x1 < x2) {x : β} {s : Set β} (hx : x ∈ s) : h.min s ⋯ ≤ x

theorem Set.range_injOn_strictMono_of_wellFoundedLT {β : Type u_2} {γ : Type u_3} [LinearOrder β] [Preorder γ] [WellFoundedLT β] : InjOn range {f : β → γ | StrictMono f}

theorem Set.range_injOn_strictMono_of_wellFoundedGT {β : Type u_2} {γ : Type u_3} [LinearOrder β] [Preorder γ] [WellFoundedGT β] : InjOn range {f : β → γ | StrictMono f}

@[deprecated Set.range_injOn_strictMono_of_wellFoundedLT (since := "2026-08-13")]

theorem Set.range_injOn_strictMono {β : Type u_2} {γ : Type u_3} [LinearOrder β] [Preorder γ] [WellFoundedLT β] : InjOn range {f : β → γ | StrictMono f}

Alias of Set.range_injOn_strictMono_of_wellFoundedLT.

theorem Set.range_injOn_strictAnti_of_wellFoundedGT {β : Type u_2} {γ : Type u_3} [LinearOrder β] [Preorder γ] [WellFoundedGT β] : InjOn range {f : β → γ | StrictAnti f}

theorem Set.range_injOn_strictAnti_of_wellFoundedLT {β : Type u_2} {γ : Type u_3} [LinearOrder β] [Preorder γ] [WellFoundedLT β] : InjOn range {f : β → γ | StrictAnti f}

@[deprecated Set.range_injOn_strictAnti_of_wellFoundedGT (since := "2026-08-13")]

theorem Set.range_injOn_strictAnti {β : Type u_2} {γ : Type u_3} [LinearOrder β] [Preorder γ] [WellFoundedGT β] : InjOn range {f : β → γ | StrictAnti f}

Alias of Set.range_injOn_strictAnti_of_wellFoundedGT.

theorem StrictMono.range_inj_of_wellFoundedLT {β : 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

theorem StrictMono.range_inj_of_wellFoundedGT {β : Type u_2} {γ : Type u_3} [LinearOrder β] [Preorder γ] [WellFoundedGT β] {f g : β → γ} (hf : StrictMono f) (hg : StrictMono g) : Set.range f = Set.range g ↔ f = g

@[deprecated StrictMono.range_inj_of_wellFoundedLT (since := "2026-08-13")]

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

Alias of StrictMono.range_inj_of_wellFoundedLT.

theorem StrictAnti.range_inj_of_wellFoundedGT {β : 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

theorem StrictAnti.range_inj_of_wellFoundedLT {β : Type u_2} {γ : Type u_3} [LinearOrder β] [Preorder γ] [WellFoundedLT β] {f g : β → γ} (hf : StrictAnti f) (hg : StrictAnti g) : Set.range f = Set.range g ↔ f = g

@[deprecated StrictAnti.range_inj_of_wellFoundedGT (since := "2026-08-13")]

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

Alias of StrictAnti.range_inj_of_wellFoundedGT.

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.

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

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

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

theorem StrictMono.apply_le {β : Type u_2} [LinearOrder β] [WellFoundedGT β] {f : β → β} (hf : StrictMono f) {x : β} : f x ≤ x

theorem StrictMono.not_bddAbove_range_of_wellFoundedLT {β : Type u_2} [LinearOrder β] {f : β → β} [WellFoundedLT β] [NoMaxOrder β] (hf : StrictMono f) : ¬BddAbove (Set.range f)

theorem StrictMono.not_bddBelow_range_of_wellFoundedGT {β : Type u_2} [LinearOrder β] {f : β → β} [WellFoundedGT β] [NoMinOrder β] (hf : StrictMono f) : ¬BddBelow (Set.range f)

noncomputable def Function.argmin {α : Type u_1} {β : Type u_2} (f : α → β) [LT β] [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.

See also Set.Finite.exists_minimalFor and related lemmas for the case when α is finite.

Equations

• Function.argmin f = ⋯.min Set.univ ⋯

noncomputable def Function.argmax {α : Type u_1} {β : Type u_2} (f : α → β) [LT β] [WellFoundedGT β] [Nonempty α] : α

Given a function f : α → β where β carries a well-founded >, this is an element of α whose image under f is maximal in the sense of Function.not_argmax_lt.

See also Set.Finite.exists_maximalFor and related lemmas for the case when α is finite.

Equations

• Function.argmax f = ⋯.min Set.univ ⋯

theorem Function.not_lt_argmin {α : Type u_1} {β : Type u_2} (f : α → β) [LT β] [WellFoundedLT β] [Nonempty α] (a : α) : ¬f a < f (argmin f)

theorem Function.not_argmax_lt {α : Type u_1} {β : Type u_2} (f : α → β) [LT β] [WellFoundedGT β] [Nonempty α] (a : α) : ¬f (argmax f) < f a

noncomputable def Function.argminOn {α : Type u_1} {β : Type u_2} (f : α → β) [LT β] [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.

See also Set.Finite.exists_minimalFor and related lemmas for the case when α or s is finite.

TODO Consider removing this definition in favour of exists_minimalFor_of_wellFoundedLT.

Equations

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

noncomputable def Function.argmaxOn {α : Type u_1} {β : Type u_2} (f : α → β) [LT β] [WellFoundedGT β] (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 maximal in the sense of Function.not_argmaxOn_lt.

See also Set.Finite.exists_maximalFor and related lemmas for the case when α or s is finite.

Equations

• Function.argmaxOn f s hs = ⋯.min s hs

@[simp]

theorem Function.argminOn_mem {α : Type u_1} {β : Type u_2} (f : α → β) [LT β] [WellFoundedLT β] (s : Set α) (hs : s.Nonempty) : argminOn f s hs ∈ s

@[simp]

theorem Function.argmaxOn_mem {α : Type u_1} {β : Type u_2} (f : α → β) [LT β] [WellFoundedGT β] (s : Set α) (hs : s.Nonempty) : argmaxOn f s hs ∈ s

theorem Function.not_lt_argminOn {α : Type u_1} {β : Type u_2} (f : α → β) [LT β] [WellFoundedLT β] (s : Set α) {a : α} (ha : a ∈ s) : ¬f a < f (argminOn f s ⋯)

theorem Function.not_argmaxOn_lt {α : Type u_1} {β : Type u_2} (f : α → β) [LT β] [WellFoundedGT β] (s : Set α) {a : α} (ha : a ∈ s) : ¬f (argmaxOn f s ⋯) < f a

theorem Function.argmin_le {α : Type u_1} {β : Type u_2} (f : α → β) [LinearOrder β] [WellFoundedLT β] (a : α) [Nonempty α] : f (argmin f) ≤ f a

theorem Function.le_argmax {α : Type u_1} {β : Type u_2} (f : α → β) [LinearOrder β] [WellFoundedGT β] (a : α) [Nonempty α] : f a ≤ f (argmax f)

theorem Function.minimalFor_argmin {α : Type u_1} {β : Type u_2} (f : α → β) [LinearOrder β] [WellFoundedLT β] [Nonempty α] : MinimalFor (fun (x : α) => True) f (argmin f)

theorem Function.maximalFor_argmax {α : Type u_1} {β : Type u_2} (f : α → β) [LinearOrder β] [WellFoundedGT β] [Nonempty α] : MaximalFor (fun (x : α) => True) f (argmax f)

@[deprecated Function.minimalFor_argmin (since := "2026-08-13")]

theorem Function.isMinimalFor_argmin {α : Type u_1} {β : Type u_2} (f : α → β) [LinearOrder β] [WellFoundedLT β] [Nonempty α] : MinimalFor (fun (x : α) => True) f (argmin f)

Alias of Function.minimalFor_argmin.

theorem Function.argminOn_le {α : Type u_1} {β : Type u_2} (f : α → β) [LinearOrder β] [WellFoundedLT β] (s : Set α) {a : α} (ha : a ∈ s) : f (argminOn f s ⋯) ≤ f a

theorem Function.le_argmaxOn {α : Type u_1} {β : Type u_2} (f : α → β) [LinearOrder β] [WellFoundedGT β] (s : Set α) {a : α} (ha : a ∈ s) : f a ≤ f (argmaxOn f s ⋯)

theorem Function.minimalFor_argminOn {α : Type u_1} {β : Type u_2} (f : α → β) [LinearOrder β] [WellFoundedLT β] (s : Set α) (hs : s.Nonempty) : MinimalFor (fun (x : α) => x ∈ s) f (argminOn f s hs)

theorem Function.maximalFor_argmaxOn {α : Type u_1} {β : Type u_2} (f : α → β) [LinearOrder β] [WellFoundedGT β] (s : Set α) (hs : s.Nonempty) : MaximalFor (fun (x : α) => x ∈ s) f (argmaxOn f s hs)

@[deprecated Function.minimalFor_argminOn (since := "2026-08-13")]

theorem Function.isMinimalFor_argminOn {α : Type u_1} {β : Type u_2} (f : α → β) [LinearOrder β] [WellFoundedLT β] (s : Set α) (hs : s.Nonempty) : MinimalFor (fun (x : α) => x ∈ s) f (argminOn f s hs)

Alias of Function.minimalFor_argminOn.

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

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.

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

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.

@[instance_reducible]

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 := WellFoundedLT.min Set.univ ⋯, bot_le := ⋯ }

@[instance_reducible]

noncomputable def WellFoundedGT.toOrderTop (α : Type u_4) [LinearOrder α] [Nonempty α] [h : WellFoundedGT α] : OrderTop α

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

Equations

• WellFoundedGT.toOrderTop α = { top := WellFoundedGT.max Set.univ ⋯, le_top := ⋯ }

instance instWellFoundedLTULift {α : Type u_1} [LT α] [h : WellFoundedLT α] : WellFoundedLT (ULift α)

instance instWellFoundedGTULift {α : Type u_1} [LT α] [h : WellFoundedGT α] : WellFoundedGT (ULift α)