eventually_iInf_range_pow_eq — Mathlib

English

For a monotone chain of submodules, stabilization holds.

Русский

Для монотонной цепи подмодулей выполняется стабилизация.

LaTeX

$$$\\exists n, \\forall m, n \\le m \\Rightarrow f(n) = f(m)$$$

Lean4

theorem eventually_iInf_range_pow_eq (f : Module.End R M) :
    ∀ᶠ n in atTop, ⨅ m, LinearMap.range (f ^ m) = LinearMap.range (f ^ n) :=
  by
  obtain ⟨n, hn : ∀ m, n ≤ m → LinearMap.range (f ^ n) = LinearMap.range (f ^ m)⟩ :=
    IsArtinian.monotone_stabilizes f.iterateRange
  refine eventually_atTop.mpr ⟨n, fun l hl ↦ le_antisymm (iInf_le _ _) (le_iInf fun m ↦ ?_)⟩
  rcases le_or_gt l m with h | h
  · rw [← hn _ (hl.trans h), hn _ hl]
  · exact f.iterateRange.monotone h.le

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