eventuallyConst_atTop_nat — Mathlib

English

For f : Nat → α, EventuallyConst f atTop is equivalent to the existence of n with a tail-stabilization condition: f(m+1) = f(m) for all m ≥ n.

Русский

Для f : Nat → α, EventuallyConst f atTop эквивалентно существованию n, для которого f(m+1) = f(m) при m ≥ n.

LaTeX

$$$\mathrm{EventuallyConst}(f,\mathrm{atTop}) \iff \exists n, \forall m, n \le m \Rightarrow f(m+1) = f(m)$$$

Lean4

theorem eventuallyConst_atTop_nat {f : ℕ → α} : EventuallyConst f atTop ↔ ∃ n, ∀ m, n ≤ m → f (m + 1) = f m :=
  by
  rw [eventuallyConst_atTop]
  refine exists_congr fun n ↦ ⟨fun h m hm ↦ ?_, fun h m hm ↦ ?_⟩
  · exact (h (m + 1) (hm.trans m.le_succ)).trans (h m hm).symm
  ·
    induction m, hm using Nat.le_induction with
    | base => rfl
    | succ m hm ihm => exact (h m hm).trans ihm

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