acc_iff_isEmpty_descending_chain — Mathlib

English

Accessibility at x is equivalent to the nonexistence of any descending chain starting at x.

Русский

Доступность x эквивалентна отсутствию какой-либо нисходящей цепи, начинающейся в x.

LaTeX

$$$Acc\ r\ x \iff IsEmpty { f : \mathbb{N} \to α \mid f(0) = x \land \forall n, r (f(n+1)) (f n) }$$$

Lean4

theorem acc_iff_isEmpty_descending_chain {α} {r : α → α → Prop} {x : α} :
    Acc r x ↔ IsEmpty { f : ℕ → α // f 0 = x ∧ ∀ n, r (f (n + 1)) (f n) } :=
  by
  rw [← not_iff_not, not_isEmpty_iff, nonempty_subtype]
  exact not_acc_iff_exists_descending_chain

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