English
Let (α, ≤) be a preorder and s ⊆ α. Then s is well-founded if and only if there is no infinite sequence f: ℕ → α with all values in s that is strictly descending with respect to ≤.
Русский
Пусть (α, ≤) — предпорядок, и s ⊆ α. Тогда множество s фундаментально по отношению ≤ тогда и только тогда, когда не существует бесконечной последовательности f: ℕ → α, все значения которой лежат в s и которая строго убывает по отношению ≤.
LaTeX
$$$IsWF(s) \\iff \\forall f:\\\\mathbb{N} \\to \\alpha, StrictAnti(f) \\to \\neg \\forall n:\\\\mathbb{N}, f(n) \\in s$$$
Lean4
theorem isWF_iff_no_descending_seq : IsWF s ↔ ∀ f : ℕ → α, StrictAnti f → ¬∀ n, f n ∈ s :=
wellFoundedOn_iff_no_descending_seq.trans
⟨fun H f hf => H ⟨⟨f, hf.injective⟩, hf.lt_iff_gt⟩, fun H f => H f fun _ _ => f.map_rel_iff.2⟩
