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 WellFounded.isAsymm {α : Type u_1} {r : α → α → Prop} (h : WellFounded r) : IsAsymm α r

theorem WellFounded.isIrrefl {α : Type u_1} {r : α → α → Prop} (h : WellFounded r) : IsIrrefl α r

instance WellFounded.instIsAsymmRel {α : Type u_1} [WellFoundedRelation α] : IsAsymm α WellFoundedRelation.rel

instance WellFounded.instIsIrreflRel {α : Type u_1} : IsIrrefl α 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)

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.

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.

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

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)

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

theorem WellFounded.wellFounded_iff_no_descending_seq {α : Type 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 decreasing sequence.

See RelEmbedding.wellFounded_iff_no_descending_seq for a version on strict orders.

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

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

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

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

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

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

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_apply {β : Type u_2} [LinearOrder β] [WellFoundedLT β] {f : β → β} (hf : StrictMono f) {x : β} : x ≤ f x

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.

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 β] [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.

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

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.

@[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

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)

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

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

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.

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

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

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

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