Documentation

Mathlib.Order.WellFounded

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) :
instance WellFounded.instIsAsymmRel {α : Type u_1} [WellFoundedRelation α] :
IsAsymm α WellFoundedRelation.rel
Equations
  • =
instance WellFounded.instIsIrreflRel {α : Type u_1} :
IsIrrefl α WellFoundedRelation.rel
Equations
  • =
theorem WellFounded.mono {α : Type u_1} {r : ααProp} {r' : ααProp} (hr : WellFounded r) (h : ∀ (a b : α), r' a br a b) :
theorem WellFounded.onFun {α : Sort u_4} {β : Sort u_5} {r : ββProp} {f : αβ} :
theorem WellFounded.has_min {α : Type u_4} {r : ααProp} (H : WellFounded r) (s : Set α) :
s.Nonemptyas, xs, ¬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 WellFounded.conditionallyCompleteLinearOrderWithBot and using Inf instead.

Equations
Instances For
    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.Nonemptyms, xs, ¬r x m
    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 : α | as, r a x} h
    Instances For
      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)
      noncomputable def WellFounded.succ {α : Type u_1} {r : ααProp} (wf : WellFounded 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 = if h : ∃ (y : α), r x y then wf.min {y : α | r x y} h else x
      Instances For
        theorem WellFounded.lt_succ {α : Type u_1} {r : ααProp} (wf : WellFounded r) {x : α} (h : ∃ (y : α), r x y) :
        r x (wf.succ x)
        theorem WellFounded.lt_succ_iff {α : Type u_1} {r : ααProp} [wo : IsWellOrder α r] {x : α} (h : ∃ (y : α), r x y) (y : α) :
        r y (.succ x) r y x y = x
        theorem WellFounded.min_le {β : Type u_2} [LinearOrder β] (h : WellFounded fun (x1 x2 : β) => x1 < x2) {x : β} {s : Set β} (hx : x s) (hne : optParam s.Nonempty ) :
        h.min s hne x
        theorem Set.range_injOn_strictMono {β : Type u_2} {γ : Type u_3} [LinearOrder β] [Preorder γ] [WellFoundedLT β] :
        Set.InjOn Set.range {f : βγ | StrictMono f}
        theorem Set.range_injOn_strictAnti {β : Type u_2} {γ : Type u_3} [LinearOrder β] [Preorder γ] [WellFoundedGT β] :
        Set.InjOn Set.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) :
        theorem StrictAnti.range_inj {β : Type u_2} {γ : Type u_3} [LinearOrder β] [Preorder γ] [WellFoundedGT β] {f : βγ} {g : βγ} (hf : StrictAnti f) (hg : StrictAnti g) :
        @[deprecated StrictMono.range_inj]
        theorem WellFounded.eq_strictMono_iff_eq_range {β : Type u_2} {γ : Type u_3} [LinearOrder β] [Preorder γ] (h : WellFounded fun (x1 x2 : β) => x1 < x2) {f : βγ} {g : βγ} (hf : StrictMono f) (hg : StrictMono 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
        @[deprecated StrictMono.le_apply]
        theorem WellFounded.self_le_of_strictMono {β : Type u_2} [LinearOrder β] (h : WellFounded fun (x1 x2 : β) => x1 < x2) {f : ββ} (hf : StrictMono f) (n : β) :
        n f n
        noncomputable def Function.argmin {α : Type u_1} {β : Type u_2} (f : αβ) [LT β] (h : WellFounded fun (x1 x2 : β) => x1 < x2) [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
        Instances For
          theorem Function.not_lt_argmin {α : Type u_1} {β : Type u_2} (f : αβ) [LT β] (h : WellFounded fun (x1 x2 : β) => x1 < x2) [Nonempty α] (a : α) :
          ¬f a < f (Function.argmin f h)
          noncomputable def Function.argminOn {α : Type u_1} {β : Type u_2} (f : αβ) [LT β] (h : WellFounded fun (x1 x2 : β) => x1 < x2) (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
          Instances For
            @[simp]
            theorem Function.argminOn_mem {α : Type u_1} {β : Type u_2} (f : αβ) [LT β] (h : WellFounded fun (x1 x2 : β) => x1 < x2) (s : Set α) (hs : s.Nonempty) :
            theorem Function.not_lt_argminOn {α : Type u_1} {β : Type u_2} (f : αβ) [LT β] (h : WellFounded fun (x1 x2 : β) => x1 < x2) (s : Set α) {a : α} (ha : a s) (hs : optParam s.Nonempty ) :
            ¬f a < f (Function.argminOn f h s hs)
            theorem Function.argmin_le {α : Type u_1} {β : Type u_2} (f : αβ) [LinearOrder β] (h : WellFounded fun (x1 x2 : β) => x1 < x2) (a : α) [Nonempty α] :
            f (Function.argmin f h) f a
            theorem Function.argminOn_le {α : Type u_1} {β : Type u_2} (f : αβ) [LinearOrder β] (h : WellFounded fun (x1 x2 : β) => x1 < x2) (s : Set α) {a : α} (ha : a s) (hs : optParam s.Nonempty ) :
            f (Function.argminOn f h 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 botC (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 botC b∃ (c : α), r c b C c) :
            C aC 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 botC (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 botC b∃ (c : α), r c b C c) :
            C aC 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.

            theorem StrictMono.wellFoundedLT {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} [WellFoundedLT β] (hf : StrictMono f) :
            theorem StrictAnti.wellFoundedLT {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} [WellFoundedGT β] (hf : StrictAnti f) :
            theorem StrictMono.wellFoundedGT {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} [WellFoundedGT β] (hf : StrictMono f) :
            theorem StrictAnti.wellFoundedGT {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : αβ} [WellFoundedLT β] (hf : StrictAnti f) :
            noncomputable def WellFoundedLT.toOrderBot {α : Type u_4} [LinearOrder α] [Nonempty α] [h : WellFoundedLT α] :

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

            Equations
            Instances For
              noncomputable def WellFoundedGT.toOrderTop {α : Type u_4} [LinearOrder α] [Nonempty α] [WellFoundedGT α] :

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

              Equations
              Instances For