English
Not having accessibility at x is equivalent to the existence of a descending chain f: Nat → α with f(0) = x and r(f(n+1)) (f(n)) for all n.
Русский
Не-Accessible x эквивалентно существованию нисходящей цепи f: Nat → α с f(0) = x и r(f(n+1)) (f(n)) для всех n.
LaTeX
$$$\neg Acc\ r\ x \iff \exists f : \mathbb{N} \to α, f(0) = x \land \forall n, r (f(n+1)) (f n)$$$
Lean4
theorem not_acc_iff_exists_descending_chain {α} {r : α → α → Prop} {x : α} :
¬Acc r x ↔ ∃ f : ℕ → α, f 0 = x ∧ ∀ n, r (f (n + 1)) (f n)
where
mp
hx :=
let f : ℕ → { a : α // ¬Acc r a } := Nat.rec ⟨x, hx⟩ fun _ a ↦ ⟨_, (exists_not_acc_lt_of_not_acc a.2).choose_spec.1⟩
⟨(f · |>.1), rfl, fun n ↦ (exists_not_acc_lt_of_not_acc (f n).2).choose_spec.2⟩
mpr h acc := acc.rec (fun _x _ ih ⟨f, hf⟩ ↦ ih (f 1) (hf.1 ▸ hf.2 0) ⟨(f <| · + 1), rfl, fun _ ↦ hf.2 _⟩) h
