le_comap_pow_of_le_comap — Mathlib

English

If q ≤ q' are submodules of M₂, then comap f q ≤ comap f q'.

Русский

Если q ⊆ q', то comap f q ⊆ comap f q'.

LaTeX

$$q \\subseteq q' \\Rightarrow comap f q \\subseteq comap f q'$$

Lean4

theorem le_comap_pow_of_le_comap (p : Submodule R M) {f : M →ₗ[R] M} (h : p ≤ p.comap f) (k : ℕ) :
    p ≤ p.comap (f ^ k) := by
  induction k with
  | zero => simp [Module.End.one_eq_id]
  | succ k ih => simp [Module.End.iterate_succ, comap_comp, h.trans (comap_mono ih)]

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