Mathlib.Order.WellFounded

WellFounded.isAsymm theorem

(h : WellFounded r) : IsAsymm α r

Full source

protected theorem isAsymm (h : WellFounded r) : IsAsymm α r := ⟨h.asymmetric⟩

Asymmetry Property of Well-Founded Relations

Informal description

For any type $\alpha$ and a well-founded relation $r$ on $\alpha$, the relation $r$ is asymmetric, meaning that for any elements $a, b \in \alpha$, if $r(a, b)$ holds then $r(b, a)$ does not hold.

WellFounded.isIrrefl theorem

(h : WellFounded r) : IsIrrefl α r

Full source

protected theorem isIrrefl (h : WellFounded r) : IsIrrefl α r := @IsAsymm.isIrrefl α r h.isAsymm

Irreflexivity Property of Well-Founded Relations

Informal description

For any type $\alpha$ and a well-founded relation $r$ on $\alpha$, the relation $r$ is irreflexive, meaning that for any element $a \in \alpha$, $r(a, a)$ does not hold.

WellFounded.instIsAsymmRel instance

[WellFoundedRelation α] : IsAsymm α WellFoundedRelation.rel

Full source

instance [WellFoundedRelation α] : IsAsymm α WellFoundedRelation.rel :=
  WellFoundedRelation.wf.isAsymm

Asymmetry of Well-Founded Relations

Informal description

For any type $\alpha$ with a well-founded relation, the relation is asymmetric.

WellFounded.instIsIrreflRel instance

: IsIrrefl α WellFoundedRelation.rel

Full source

instance : IsIrrefl α WellFoundedRelation.rel := IsAsymm.isIrrefl

Irreflexivity of Well-Founded Relations

Informal description

For any type $\alpha$ with a well-founded relation, the relation is irreflexive.

WellFounded.mono theorem

(hr : WellFounded r) (h : ∀ a b, r' a b → r a b) : WellFounded r'

Full source

theorem mono (hr : WellFounded r) (h : ∀ a b, r' a b → r a b) : WellFounded r' :=
  Subrelation.wf (h _ _) hr

Well-foundedness is preserved under relation strengthening

Informal description

Let $r$ and $r'$ be binary relations on a type $\alpha$. If $r$ is well-founded and $r'$ implies $r$ (i.e., for all $a, b \in \alpha$, $r' a b$ implies $r a b$), then $r'$ is also well-founded.

WellFounded.onFun theorem

{α β : Sort*} {r : β → β → Prop} {f : α → β} : WellFounded r → WellFounded (r on f)

Full source

theorem onFun {α β : Sort*} {r : β → β → Prop} {f : α → β} :
    WellFounded r → WellFounded (r on f) :=
  InvImage.wf _

Well-foundedness is preserved under function-induced relations

Informal description

Let $\alpha$ and $\beta$ be types, $r$ be a binary relation on $\beta$, and $f \colon \alpha \to \beta$ be a function. If $r$ is well-founded, then the relation $r \text{ on } f$ defined by $(r \text{ on } f)(x, y) = r(f(x), f(y))$ is also well-founded on $\alpha$.

WellFounded.has_min theorem

{α} {r : α → α → Prop} (H : WellFounded r) (s : Set α) : s.Nonempty → ∃ a ∈ s, ∀ x ∈ s, ¬r x a

Full source

/-- If `r` is a well-founded relation, then any nonempty set has a minimal element
with respect to `r`. -/
theorem has_min {α} {r : α → α → Prop} (H : WellFounded r) (s : Set α) :
    s.Nonempty → ∃ a ∈ s, ∀ x ∈ s, ¬r x a
  | ⟨a, ha⟩ => show ∃ b ∈ s, ∀ x ∈ s, ¬r x b from
    Acc.recOn (H.apply a) (fun x _ IH =>
        not_imp_not.1 fun hne hx => hne <| ⟨x, hx, fun y hy hyx => hne <| IH y hyx hy⟩)
      ha

Existence of Minimal Elements in Nonempty Sets under Well-Founded Relations

Informal description

Let $\alpha$ be a type and $r$ be a well-founded relation on $\alpha$. For any nonempty subset $s$ of $\alpha$, there exists an element $a \in s$ such that for all $x \in s$, $\neg r(x, a)$. In other words, every nonempty set has a minimal element with respect to $r$.

WellFounded.min definition

{r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : s.Nonempty) : α

Full source

/-- 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. -/
noncomputable def min {r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : s.Nonempty) : α :=
  Classical.choose (H.has_min s h)

Minimal element in a nonempty set under a well-founded relation

Informal description

Given a well-founded relation $r$ on a type $\alpha$ and a nonempty subset $s$ of $\alpha$, the function $\mathrm{min}$ returns an element of $s$ that is minimal with respect to $r$. That is, for any $x \in s$, $\neg r(x, \mathrm{min}(s))$.

WellFounded.min_mem theorem

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

Full source

theorem min_mem {r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : s.Nonempty) :
    H.min s h ∈ s :=
  let ⟨h, _⟩ := Classical.choose_spec (H.has_min s h)
  h

Membership of Minimal Element in Nonempty Set under Well-Founded Relation

Informal description

For any well-founded relation $r$ on a type $\alpha$ and any nonempty subset $s \subseteq \alpha$, the minimal element $\mathrm{min}(s)$ with respect to $r$ belongs to $s$.

WellFounded.not_lt_min theorem

{r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : s.Nonempty) {x} (hx : x ∈ s) : ¬r x (H.min s h)

Full source

theorem not_lt_min {r : α → α → Prop} (H : WellFounded r) (s : Set α) (h : s.Nonempty) {x}
    (hx : x ∈ s) : ¬r x (H.min s h) :=
  let ⟨_, h'⟩ := Classical.choose_spec (H.has_min s h)
  h' _ hx

Minimal Element Property in Well-Founded Relations: $\neg r(x, \mathrm{min}_r(s))$ for $x \in s$

Informal description

Let $\alpha$ be a type with a well-founded relation $r$, and let $s$ be a nonempty subset of $\alpha$. For any element $x \in s$, it is not the case that $x$ is related to the minimal element of $s$ under $r$, i.e., $\neg r(x, \mathrm{min}_r(s))$.

WellFounded.wellFounded_iff_has_min theorem

{r : α → α → Prop} : WellFounded r ↔ ∀ s : Set α, s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m

Full source

theorem wellFounded_iff_has_min {r : α → α → Prop} :
    WellFoundedWellFounded r ↔ ∀ s : Set α, s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m := by
  refine ⟨fun h => h.has_min, fun h => ⟨fun x => ?_⟩⟩
  by_contra hx
  obtain ⟨m, hm, hm'⟩ := h {x | ¬Acc r x} ⟨x, hx⟩
  refine hm ⟨_, fun y hy => ?_⟩
  by_contra hy'
  exact hm' y hy' hy

Characterization of Well-Founded Relations via Minimal Elements

Informal description

A relation $r$ on a type $\alpha$ is well-founded if and only if every nonempty subset $s \subseteq \alpha$ has a minimal element with respect to $r$, i.e., there exists $m \in s$ such that for all $x \in s$, $\neg r(x, m)$.

WellFounded.wellFounded_iff_no_descending_seq theorem

: WellFounded r ↔ IsEmpty { f : ℕ → α // ∀ n, r (f (n + 1)) (f n) }

Full source

/-- 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_iff_no_descending_seq :
    WellFoundedWellFounded r ↔ IsEmpty { f : ℕ → α // ∀ n, r (f (n + 1)) (f n) } := by
  rw [WellFounded.wellFounded_iff_has_min]
  refine ⟨fun hr ↦ ⟨fun ⟨f, hf⟩ ↦ ?_⟩, ?_⟩
  · obtain ⟨_, ⟨n, rfl⟩, hn⟩ := hr _ (Set.range_nonempty f)
    exact hn _ (Set.mem_range_self (n + 1)) (hf n)
  · contrapose!
    rw [not_isEmpty_iff]
    rintro ⟨s, hs, hs'⟩
    let f : ℕ → s := Nat.rec (Classical.indefiniteDescription _ hs) fun n IH ↦
      ⟨(hs' _ IH.2).choose, (hs' _ IH.2).choose_spec.1⟩
    exact ⟨⟨Subtype.val ∘ f, fun n ↦ (hs' _ (f n).2).choose_spec.2⟩⟩

Characterization of Well-Founded Relations via Absence of Infinite Descending Sequences

Informal description

A relation $r$ on a type $\alpha$ is well-founded if and only if there does not exist any infinite descending sequence $(f(n))_{n \in \mathbb{N}}$ in $\alpha$ such that $r(f(n+1), f(n))$ holds for all $n \in \mathbb{N}$.

WellFounded.not_rel_apply_succ theorem

[h : IsWellFounded α r] (f : ℕ → α) : ∃ n, ¬r (f (n + 1)) (f n)

Full source

theorem not_rel_apply_succ [h : IsWellFounded α r] (f : ℕ → α) : ∃ n, ¬ r (f (n + 1)) (f n) := by
  by_contra! hf
  exact (wellFounded_iff_no_descending_seq.1 h.wf).elim ⟨f, hf⟩

No Infinite Descending Sequences in Well-Founded Relations

Informal description

For any well-founded relation $r$ on a type $\alpha$ and any sequence $f \colon \mathbb{N} \to \alpha$, there exists a natural number $n$ such that $\neg r(f(n+1), f(n))$.

WellFounded.sup definition

{r : α → α → Prop} (wf : WellFounded r) (s : Set α) (h : Bounded r s) : α

Full source

/-- The supremum of a bounded, well-founded order -/
protected noncomputable def sup {r : α → α → Prop} (wf : WellFounded r) (s : Set α)
    (h : Bounded r s) : α :=
  wf.min { x | ∀ a ∈ s, r a x } h

Supremum with respect to a well-founded relation

Informal description

Given a well-founded relation $r$ on a type $\alpha$ and a bounded subset $s$ of $\alpha$, the function $\mathrm{sup}$ returns an element $x$ of $\alpha$ such that for every $a \in s$, the relation $r(a, x)$ holds. This element $x$ is minimal among all such elements with respect to $r$.

WellFounded.lt_sup theorem

{r : α → α → Prop} (wf : WellFounded r) {s : Set α} (h : Bounded r s) {x} (hx : x ∈ s) : r x (wf.sup s h)

Full source

protected theorem lt_sup {r : α → α → Prop} (wf : WellFounded r) {s : Set α} (h : Bounded r s) {x}
    (hx : x ∈ s) : r x (wf.sup s h) :=
  min_mem wf { x | ∀ a ∈ s, r a x } h x hx

Elements of a Bounded Set are Related to its Supremum under a Well-Founded Relation

Informal description

Let $r$ be a well-founded relation on a type $\alpha$, and let $s$ be a bounded subset of $\alpha$ with respect to $r$. For any element $x \in s$, the relation $r(x, \mathrm{sup}(s))$ holds, where $\mathrm{sup}(s)$ is the supremum of $s$ with respect to $r$.

WellFounded.succ definition

{r : α → α → Prop} (wf : WellFounded r) (x : α) : α

Full source

/-- 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. -/
@[deprecated "If you have a linear order, consider defining a `SuccOrder` instance through
`ConditionallyCompleteLinearOrder.toSuccOrder`." (since := "2024-10-25")]
protected noncomputable def succ {r : α → α → Prop} (wf : WellFounded r) (x : α) : α :=
  if h : ∃ y, r x y then wf.min { y | r x y } h else x

Successor in a well-founded order

Informal description

Given a well-founded relation $r$ on a type $\alpha$ and an element $x \in \alpha$, the successor of $x$ with respect to $r$ is defined as follows: if there exists some $y$ such that $r(x, y)$, then the successor is the minimal such $y$ (with respect to $r$); otherwise, the successor is $x$ itself.

WellFounded.lt_succ theorem

{r : α → α → Prop} (wf : WellFounded r) {x : α} (h : ∃ y, r x y) : r x (wf.succ x)

Full source

@[deprecated "`WellFounded.succ` is deprecated" (since := "2024-10-25")]
protected theorem lt_succ {r : α → α → Prop} (wf : WellFounded r) {x : α} (h : ∃ y, r x y) :
    r x (wf.succ x) := by
  rw [WellFounded.succ, dif_pos h]
  apply min_mem

Successor Relation in Well-Founded Order: $x < \mathrm{succ}(x)$

Informal description

Let $r$ be a well-founded relation on a type $\alpha$. For any element $x \in \alpha$ such that there exists $y$ with $r(x, y)$, the successor of $x$ with respect to $r$ satisfies $r(x, \mathrm{succ}(x))$.

WellFounded.lt_succ_iff theorem

 {r : α → α → Prop} [wo : IsWellOrder α r] {x : α} (h : ∃ y, r x y) (y : α) : r y (wo.wf.succ x) ↔ r y x ∨ y = x

Full source

@[deprecated "`WellFounded.succ` is deprecated" (since := "2024-10-25")]
protected theorem lt_succ_iff {r : α → α → Prop} [wo : IsWellOrder α r] {x : α} (h : ∃ y, r x y)
    (y : α) : r y (wo.wf.succ x) ↔ r y x ∨ y = x := by
  constructor
  · intro h'
    have : ¬r x y := by
      intro hy
      rw [WellFounded.succ, dif_pos] at h'
      exact wo.wf.not_lt_min _ h hy h'
    rcases trichotomous_of r x y with (hy | hy | hy)
    · exfalso
      exact this hy
    · right
      exact hy.symm
    left
    exact hy
  rintro (hy | rfl); (· exact _root_.trans hy (wo.wf.lt_succ h)); exact wo.wf.lt_succ h

Characterization of Successor in Well-Orders: $y < \mathrm{succ}(x) \leftrightarrow y < x \lor y = x$

Informal description

Let $\alpha$ be a type equipped with a well-order relation $r$. For any element $x \in \alpha$ such that there exists $y$ with $r(x, y)$, and for any $y \in \alpha$, we have $r(y, \mathrm{succ}(x))$ if and only if either $r(y, x)$ or $y = x$.

Set.range_injOn_strictMono theorem

[WellFoundedLT β] : Set.InjOn Set.range {f : β → γ | StrictMono f}

Full source

theorem Set.range_injOn_strictMono [WellFoundedLT β] :
    Set.InjOn Set.range { f : β → γ | StrictMono f } := by
  intro f hf g hg hfg
  ext a
  apply WellFoundedLT.induction a
  intro a IH
  obtain ⟨b, hb⟩ := hfg ▸ mem_range_self a
  obtain h | rfl | h := lt_trichotomy b a
  · rw [← IH b h] at hb
    cases (hf.injective hb).not_lt h
  · rw [hb]
  · obtain ⟨c, hc⟩ := hfg.symm ▸ mem_range_self a
    have := hg h
    rw [hb, ← hc, hf.lt_iff_lt] at this
    rw [IH c this] at hc
    cases (hg.injective hc).not_lt this

Injectivity of Range for Strictly Monotone Functions over Well-Founded Domains

Informal description

Let $\beta$ be a type with a well-founded strict less-than relation $<$. Then the range function $\mathrm{range} : (\beta \to \gamma) \to \mathrm{Set}(\gamma)$ is injective when restricted to the set of strictly monotone functions from $\beta$ to $\gamma$. In other words, if $f, g : \beta \to \gamma$ are strictly monotone and have the same range, then $f = g$.

Set.range_injOn_strictAnti theorem

[WellFoundedGT β] : Set.InjOn Set.range {f : β → γ | StrictAnti f}

Full source

theorem Set.range_injOn_strictAnti [WellFoundedGT β] :
    Set.InjOn Set.range { f : β → γ | StrictAnti f } :=
  fun _ hf _ hg ↦ Set.range_injOn_strictMono (β := βᵒᵈ) hf.dual hg.dual

Injectivity of Range for Strictly Antitone Functions over Well-Founded Domains

Informal description

Let $\beta$ be a type with a well-founded strict greater-than relation $>$. Then the range function $\mathrm{range} : (\beta \to \gamma) \to \mathrm{Set}(\gamma)$ is injective when restricted to the set of strictly antitone functions from $\beta$ to $\gamma$. In other words, if $f, g : \beta \to \gamma$ are strictly antitone and have the same range, then $f = g$.

StrictMono.range_inj theorem

[WellFoundedLT β] {f g : β → γ} (hf : StrictMono f) (hg : StrictMono g) : Set.range f = Set.range g ↔ f = g

Full source

theorem StrictMono.range_inj [WellFoundedLT β] {f g : β → γ}
    (hf : StrictMono f) (hg : StrictMono g) : Set.rangeSet.range f = Set.range g ↔ f = g :=
  Set.range_injOn_strictMono.eq_iff hf hg

Injectivity of Range for Strictly Monotone Functions on Well-Founded Domains

Informal description

Let $\beta$ be a type with a well-founded strict less-than relation $<$, and let $f, g : \beta \to \gamma$ be strictly monotone functions. Then the ranges of $f$ and $g$ are equal if and only if $f = g$.

StrictAnti.range_inj theorem

[WellFoundedGT β] {f g : β → γ} (hf : StrictAnti f) (hg : StrictAnti g) : Set.range f = Set.range g ↔ f = g

Full source

theorem StrictAnti.range_inj [WellFoundedGT β] {f g : β → γ}
    (hf : StrictAnti f) (hg : StrictAnti g) : Set.rangeSet.range f = Set.range g ↔ f = g :=
  Set.range_injOn_strictAnti.eq_iff hf hg

Injectivity of Range for Strictly Antitone Functions on Well-Founded Domains

Informal description

Let $\beta$ be a type with a well-founded strict greater-than relation $>$, and let $f, g : \beta \to \gamma$ be strictly antitone functions. Then the ranges of $f$ and $g$ are equal if and only if $f = g$.

StrictMono.id_le theorem

[WellFoundedLT β] {f : β → β} (hf : StrictMono f) : id ≤ f

Full source

/-- A strictly monotone function `f` on a well-order satisfies `x ≤ f x` for all `x`. -/
theorem StrictMono.id_le [WellFoundedLT β] {f : β → β} (hf : StrictMono f) : id ≤ f := by
  rw [Pi.le_def]
  by_contra! H
  obtain ⟨m, hm, hm'⟩ := wellFounded_lt.has_min _ H
  exact hm' _ (hf hm) hm

Strictly Monotone Functions Dominate the Identity on Well-Founded Orders

Informal description

Let $\beta$ be a type with a well-founded strict less-than relation $<$, and let $f : \beta \to \beta$ be a strictly monotone function. Then for every $x \in \beta$, we have $x \leq f(x)$.

StrictMono.le_apply theorem

[WellFoundedLT β] {f : β → β} (hf : StrictMono f) {x} : x ≤ f x

Full source

theorem StrictMono.le_apply [WellFoundedLT β] {f : β → β} (hf : StrictMono f) {x} : x ≤ f x :=
  hf.id_le x

Strictly Monotone Functions Dominate the Identity on Well-Founded Orders

Informal description

Let $\beta$ be a type with a well-founded strict less-than relation $<$, and let $f : \beta \to \beta$ be a strictly monotone function. Then for every $x \in \beta$, we have $x \leq f(x)$.

StrictMono.le_id theorem

[WellFoundedGT β] {f : β → β} (hf : StrictMono f) : f ≤ id

Full source

/-- A strictly monotone function `f` on a cowell-order satisfies `f x ≤ x` for all `x`. -/
theorem StrictMono.le_id [WellFoundedGT β] {f : β → β} (hf : StrictMono f) : f ≤ id :=
  StrictMono.id_le (β := βᵒᵈ) hf.dual

Strictly Monotone Functions are Bounded Above by Identity on Well-Founded Orders

Informal description

Let $\beta$ be a type with a well-founded strict greater-than relation $>$, and let $f : \beta \to \beta$ be a strictly monotone function. Then for every $x \in \beta$, we have $f(x) \leq x$.

StrictMono.apply_le theorem

[WellFoundedGT β] {f : β → β} (hf : StrictMono f) {x} : f x ≤ x

Full source

theorem StrictMono.apply_le [WellFoundedGT β] {f : β → β} (hf : StrictMono f) {x} : f x ≤ x :=
  StrictMono.le_apply (β := βᵒᵈ) hf.dual

Strictly Monotone Functions are Bounded Above by Identity on Well-Founded Orders with $>$

Informal description

Let $\beta$ be a type with a well-founded strict greater-than relation $>$, and let $f : \beta \to \beta$ be a strictly monotone function. Then for every $x \in \beta$, we have $f(x) \leq x$.

StrictMono.not_bddAbove_range_of_wellFoundedLT theorem

{f : β → β} [WellFoundedLT β] [NoMaxOrder β] (hf : StrictMono f) : ¬BddAbove (Set.range f)

Full source

theorem StrictMono.not_bddAbove_range_of_wellFoundedLT {f : β → β} [WellFoundedLT β] [NoMaxOrder β]
    (hf : StrictMono f) : ¬ BddAbove (Set.range f) := by
  rintro ⟨a, ha⟩
  obtain ⟨b, hb⟩ := exists_gt a
  exact ((hf.le_apply.trans_lt (hf hb)).trans_le <| ha (Set.mem_range_self _)).false

Range of Strictly Monotone Function is Unbounded Above in Well-Founded Order Without Maxima

Informal description

Let $\beta$ be a type with a well-founded strict less-than relation $<$ and no maximal elements. For any strictly monotone function $f : \beta \to \beta$, the range of $f$ is not bounded above.

StrictMono.not_bddBelow_range_of_wellFoundedGT theorem

{f : β → β} [WellFoundedGT β] [NoMinOrder β] (hf : StrictMono f) : ¬BddBelow (Set.range f)

Full source

theorem StrictMono.not_bddBelow_range_of_wellFoundedGT {f : β → β} [WellFoundedGT β] [NoMinOrder β]
    (hf : StrictMono f) : ¬ BddBelow (Set.range f) :=
  hf.dual.not_bddAbove_range_of_wellFoundedLT

Range of Strictly Monotone Function is Unbounded Below in Well-Founded Order Without Minima

Informal description

Let $\beta$ be a type with a well-founded strict greater-than relation $>$ and no minimal elements. For any strictly monotone function $f : \beta \to \beta$, the range of $f$ is not bounded below.

Function.argmin definition

[Nonempty α] : α

Full source

/-- 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`. -/
noncomputable def argmin [Nonempty α] : α :=
  WellFounded.min (InvImage.wf f h.wf) Set.univ Set.univ_nonempty

Minimal argument of a function with respect to a well-founded order

Informal description

Given a function $f : \alpha \to \beta$ where $\beta$ is equipped with a well-founded strict less-than relation $<$, the element $\mathrm{argmin}\, f$ is an element of $\alpha$ whose image under $f$ is minimal in the sense that there does not exist any $a \in \alpha$ such that $f(a) < f(\mathrm{argmin}\, f)$. This is constructed using the well-foundedness of $<$ on $\beta$ to find a minimal element in the image of $f$ over the universal set of $\alpha$.

Function.not_lt_argmin theorem

[Nonempty α] (a : α) : ¬f a < f (argmin f)

Full source

theorem not_lt_argmin [Nonempty α] (a : α) : ¬f a < f (argmin f) :=
  WellFounded.not_lt_min (InvImage.wf f h.wf) _ _ (Set.mem_univ a)

Minimality of $\mathrm{argmin}\, f$ with respect to a well-founded order

Informal description

For any nonempty type $\alpha$ and any function $f : \alpha \to \beta$ where $\beta$ is equipped with a well-founded strict order $<$, there does not exist an element $a \in \alpha$ such that $f(a) < f(\mathrm{argmin}\, f)$. In other words, $\mathrm{argmin}\, f$ is a minimal element of $f$ with respect to the well-founded order $<$ on $\beta$.

Function.argminOn definition

(s : Set α) (hs : s.Nonempty) : α

Full source

/-- 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`. -/
noncomputable def argminOn (s : Set α) (hs : s.Nonempty) : α :=
  WellFounded.min (InvImage.wf f h.wf) s hs

Minimal element with respect to a function on a nonempty set

Informal description

Given a function $f : \alpha \to \beta$ where $\beta$ is equipped with a well-founded strict order $<$, and a nonempty subset $s$ of $\alpha$, the function $\mathrm{argminOn}$ returns an element of $s$ whose image under $f$ is minimal in the sense that no other element in $s$ has a strictly smaller image under $f$. More formally, for any $a \in s$, we have $\neg (f(a) < f(\mathrm{argminOn}(f, s, hs)))$, where $hs$ is a proof that $s$ is nonempty.

Function.argminOn_mem theorem

(s : Set α) (hs : s.Nonempty) : argminOn f s hs ∈ s

Full source

@[simp]
theorem argminOn_mem (s : Set α) (hs : s.Nonempty) : argminOnargminOn f s hs ∈ s :=
  WellFounded.min_mem _ _ _

Membership of Minimal Element in Nonempty Set under Well-Founded Order

Informal description

For any nonempty subset $s$ of a type $\alpha$ and a function $f : \alpha \to \beta$ where $\beta$ is equipped with a well-founded strict order $<$, the element $\mathrm{argminOn}(f, s, hs)$ belongs to $s$. Here, $hs$ is a proof that $s$ is nonempty.

Function.argmin_le theorem

(a : α) [Nonempty α] : f (argmin f) ≤ f a

Full source

theorem argmin_le (a : α) [Nonempty α] : f (argmin f) ≤ f a :=
  not_lt.mp <| not_lt_argmin f a

Minimality of $\mathrm{argmin}\, f$ with respect to a well-founded order

Informal description

For any nonempty type $\alpha$ and any function $f : \alpha \to \beta$ where $\beta$ is equipped with a well-founded strict order $<$, the image of $\mathrm{argmin}\, f$ under $f$ is less than or equal to the image of any element $a \in \alpha$ under $f$, i.e., $f(\mathrm{argmin}\, f) \leq f(a)$ for all $a \in \alpha$.

Acc.induction_bot' theorem

 {α β} {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)

Full source

/-- 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' {α β} {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) :=
  (@Acc.recOn _ _ (fun x _ => C (f x) → C (f bot)) _ ha) fun x _ ih' hC =>
    (eq_or_ne (f x) (f bot)).elim (fun h => h ▸ hC) (fun h =>
      let ⟨y, hy₁, hy₂⟩ := ih x h hC
      ih' y hy₁ hy₂)

Bottom-up induction principle for accessible elements via a function $f$

Informal description

Let $r$ be a relation on a type $\alpha$, let $f : \alpha \to \beta$ be a function, and let $C : \beta \to \mathrm{Prop}$ be a predicate. Suppose $a$ and $\mathrm{bot}$ are elements of $\alpha$ such that $a$ is accessible with respect to $r$. If the following conditions hold: 1. There exists an accessible element $a$ such that $C(f(a))$ holds. 2. For every $b$ such that $f(b) \neq f(\mathrm{bot})$ and $C(f(b))$ holds, there exists $c$ satisfying $r(c, b)$ and $C(f(c))$ holds. Then $C(f(a))$ implies $C(f(\mathrm{bot}))$.

Acc.induction_bot theorem

 {α} {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

Full source

/-- 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 Acc.induction_bot {α} {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 :=
  ha.induction_bot' ih

Bottom-up Induction Principle for Accessible Elements

Informal description

Let $r$ be a relation on a type $\alpha$, and let $C : \alpha \to \mathrm{Prop}$ be a predicate. Suppose $a$ and $\mathrm{bot}$ are elements of $\alpha$ such that $a$ is accessible with respect to $r$. If the following conditions hold: 1. $C(a)$ holds. 2. For every $b \neq \mathrm{bot}$ such that $C(b)$ holds, there exists $c$ satisfying $r(c, b)$ and $C(c)$ holds. Then $C(a)$ implies $C(\mathrm{bot})$.

WellFounded.induction_bot' theorem

 {α β} {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)

Full source

/-- 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' {α β} {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) :=
  (hwf.apply a).induction_bot' ih

Bottom-up Induction Principle for Well-founded Relations via a Function $f$

Informal description

Let $r$ be a well-founded relation on a type $\alpha$, and let $f : \alpha \to \beta$ be a function. Given a predicate $C : \beta \to \mathrm{Prop}$ and elements $a, \mathrm{bot} \in \alpha$, suppose the following conditions hold: 1. There exists an element $a$ such that $C(f(a))$ holds. 2. For every $b \in \alpha$ with $f(b) \neq f(\mathrm{bot})$ and $C(f(b))$ true, there exists $c \in \alpha$ such that $r(c, b)$ holds and $C(f(c))$ is true. Then $C(f(a))$ implies $C(f(\mathrm{bot}))$.

WellFounded.induction_bot theorem

 {α} {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

Full source

/-- 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 WellFounded.induction_bot {α} {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 :=
  hwf.induction_bot' ih

Bottom-up Induction Principle for Well-founded Relations

Informal description

Let $r$ be a well-founded relation on a type $\alpha$, and let $C : \alpha \to \mathrm{Prop}$ be a predicate. Given elements $a, \mathrm{bot} \in \alpha$, suppose the following conditions hold: 1. $C(a)$ holds. 2. For every $b \neq \mathrm{bot}$ such that $C(b)$ holds, there exists $c \in \alpha$ satisfying $r(c, b)$ and $C(c)$ holds. Then $C(a)$ implies $C(\mathrm{bot})$.

WellFoundedLT.toOrderBot definition

{α} [LinearOrder α] [Nonempty α] [h : WellFoundedLT α] : OrderBot α

Full source

/-- A nonempty linear order with well-founded `<` has a bottom element. -/
noncomputable def WellFoundedLT.toOrderBot {α} [LinearOrder α] [Nonempty α] [h : WellFoundedLT α] :
    OrderBot α where
  bot := h.wf.min _ Set.univ_nonempty
  bot_le a := h.wf.min_le (Set.mem_univ a)

Bottom element induced by well-founded less-than relation on a linear order

Informal description

Given a nonempty linearly ordered type $\alpha$ with a well-founded strict less-than relation $<$, the structure `OrderBot` is defined where the bottom element $\bot$ is the minimal element of $\alpha$ with respect to $<$, and $\bot \leq a$ holds for every $a \in \alpha$.

WellFoundedGT.toOrderTop definition

{α} [LinearOrder α] [Nonempty α] [WellFoundedGT α] : OrderTop α

Full source

/-- A nonempty linear order with well-founded `>` has a top element. -/
noncomputable def WellFoundedGT.toOrderTop {α} [LinearOrder α] [Nonempty α] [WellFoundedGT α] :
    OrderTop α :=
  have := WellFoundedLT.toOrderBot (α := αᵒᵈ)
  inferInstanceAs (OrderTop αᵒᵈαᵒᵈᵒᵈ)

Existence of top element in a well-founded linear order with $>$

Informal description

A nonempty linearly ordered set $\alpha$ with a well-founded "greater than" relation $>$ has a greatest element $\top$ (i.e., satisfies `OrderTop`).