stable_iff_exists_pow_smul_eq_of_ge

English

Equivalence between stability and the existence of the pow_smul description.

Русский

Эквивалентность устойчивости и существования pow_smul описания.

LaTeX

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

Lean4

theorem stable_iff_exists_pow_smul_eq_of_ge : F.Stable ↔ ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀ :=
  by
  refine ⟨Stable.exists_pow_smul_eq_of_ge, fun h => ⟨h.choose, fun n hn => ?_⟩⟩
  rw [h.choose_spec n hn, h.choose_spec (n + 1) (by cutsat), smul_smul, ← pow_succ', tsub_add_eq_add_tsub hn]

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