exists_pow_smul_eq_of_ge — Mathlib

English

If F.Stable, exists n0 such that for all n ≥ n0, F.N n = I^{n-n0} · F.N n0; and similar for n+1.

Русский

Если F устойчивa, существует n0: для n ≥ n0 выполняется F.N n = I^{n-n0} · F.N n0; аналогично для n+1.

LaTeX

$$∃ n₀, ∀ n ≥ n₀, F.N n = I^{n-n₀} · F.N n₀$$

Lean4

theorem exists_pow_smul_eq_of_ge (h : F.Stable) : ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀ :=
  by
  obtain ⟨n₀, hn₀⟩ := h.exists_pow_smul_eq
  use n₀
  intro n hn
  convert hn₀ (n - n₀)
  rw [add_comm, tsub_add_cancel_of_le hn]

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