not_rel_apply_succ — Mathlib

English

If r is well-founded, then for any function f: ℕ → α, there exists n such that ¬ r (f(n+1)) (f(n)).

Русский

Если r хорошо основано, то для любой функции f: ℕ → α существует число n такое, что не выполняется r (f(n+1)) (f(n)).

LaTeX

$$$\\forall f:\\mathbb{N}\\to \\alpha,\\; \\exists n:\\mathbb{N},\\; \\neg r\\,(f(n+1))\\,(f(n))$$$

Lean4

theorem not_rel_apply_succ [h : IsWellFounded α r] (f : ℕ → α) : ∃ n, ¬r (f (n + 1)) (f n) :=
  by
  by_contra! hf
  exact (wellFounded_iff_isEmpty_descending_chain.1 h.wf).elim ⟨f, hf⟩

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