English
For a linear map f: M → M, define the ranges of its iterates: range(f^n). This gives a monotone decreasing sequence of submodules of M, i.e., range(f^n) ⊇ range(f^{n+1}).
Русский
Для линейного отображения f: M → M задаём последовательность диапазонов его итераций: range(f^n). Это монотонно убывающая последовательность подпроствах M, то есть range(f^n) ⊇ range(f^{n+1}).
LaTeX
$$$n \le m \Rightarrow \operatorname{range}(f^m) \subseteq \operatorname{range}(f^n)$$$
Lean4
/-- The decreasing sequence of submodules consisting of the ranges of the iterates of a linear map.
-/
@[simps]
def iterateRange (f : M →ₗ[R] M) : ℕ →o (Submodule R M)ᵒᵈ
where
toFun n := LinearMap.range (f ^ n)
monotone' n m w x
h := by
obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_le w
rw [LinearMap.mem_range] at h
obtain ⟨m, rfl⟩ := h
rw [LinearMap.mem_range]
use (f ^ c) m
rw [pow_add, Module.End.mul_apply]
