English
A set s is well-founded under r if and only if there is no infinite descending sequence in s with respect to r.
Русский
Множество s хорошо основано по r тогда и только тогда, когда внутри s не существует бесконечной нисходящей последовательности относительно r.
LaTeX
$$s.WellFoundedOn r \\iff ∀ f : ℕ → α, (∀ n, f(n+1) r f(n) ∧ ∀ n, f(n) ∈ s) → False$$
Lean4
theorem wellFoundedOn_iff_no_descending_seq : s.WellFoundedOn r ↔ ∀ f : ((· > ·) : ℕ → ℕ → Prop) ↪r r, ¬∀ n, f n ∈ s :=
by
simp only [wellFoundedOn_iff, RelEmbedding.wellFounded_iff_isEmpty, ← not_exists, ← not_nonempty_iff, not_iff_not]
constructor
· rintro ⟨⟨f, hf⟩⟩
have H : ∀ n, f n ∈ s := fun n => (hf.2 n.lt_succ_self).2.2
refine ⟨⟨f, ?_⟩, H⟩
simpa only [H, and_true] using @hf
· rintro ⟨⟨f, hf⟩, hfs : ∀ n, f n ∈ s⟩
refine ⟨⟨f, ?_⟩⟩
simpa only [hfs, and_true] using @hf
