pow_apply_mem_of_forall_mem — Mathlib

English

If a linear endomorphism f' preserves a submodule p (i.e., f'(p) ⊆ p), then for every n, (f')^n(p) ⊆ p; in particular, (f'^n)(x) ∈ p whenever x ∈ p.

Русский

Если линейное отображение f' сохраняет подпространство p, то для любого n оно сохраняет p: (f')^n(p) ⊆ p; следовательно, при x ∈ p имеет место (f'^n)(x) ∈ p.

LaTeX

$$$\\forall n\\in\\mathbb{N},\\ (\\forall x\\in p,\; f'x\\in p)\\Rightarrow (f'^n)x\\in p$.$$

Lean4

theorem _root_.Module.End.pow_apply_mem_of_forall_mem {p : Submodule R M} (n : ℕ) (h : ∀ x ∈ p, f' x ∈ p) (x : M)
    (hx : x ∈ p) : (f' ^ n) x ∈ p := by
  induction n generalizing x with
  | zero => simpa
  | succ n ih => simpa only [iterate_succ, coe_comp, Function.comp_apply, restrict_apply] using ih _ (h _ hx)

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