wellFounded — Mathlib

English

From a well-quasi-ordered relation r, the strict part r(a,b) and not r(b,a) is a well-founded relation.

Русский

Из хорошо-квазиупорядоченного отношения r следует, что строгая часть r(a,b) и не r(b,a) образует WellFounded.

LaTeX

$$$\\text{WellQuasiOrdered}(r) \\Rightarrow \\mathrm{WellFounded}(\\lambda a b. r(a,b) \\wedge \\neg r(b,a))$$$

Lean4

theorem wellFounded {α : Type*} {r : α → α → Prop} [IsPreorder α r] (h : WellQuasiOrdered r) :
    WellFounded fun a b ↦ r a b ∧ ¬r b a :=
  by
  let _ : Preorder α :=
    { le := r
      le_refl := refl_of r
      le_trans := fun _ _ _ => trans_of r }
  have : WellQuasiOrderedLE α := ⟨h⟩
  exact wellFounded_lt

Похожие утверждения