map_subtype_mem_of_mem_invtSubmodule

English

If p is f-invariant and q is invariant in the restricted endomorphism on p, then the image of q under the inclusion map p ↪ M is f-invariant.

Русский

Если p инвариантно относительно f и q инвариантно относительно ограничения f на p, то образ q через включение p ↪ M инвариантно относительно f.

LaTeX

$$hp : p ∈ f.invtSubmodule ∧ hq : q ∈ invtSubmodule (LinearMap.restrict f hp) ⇒ Submodule.map p.subtype q ∈ f.invtSubmodule$$

Lean4

theorem map_subtype_mem_of_mem_invtSubmodule {p : Submodule R M} (hp : p ∈ f.invtSubmodule) {q : Submodule R p}
    (hq : q ∈ invtSubmodule (LinearMap.restrict f hp)) : Submodule.map p.subtype q ∈ f.invtSubmodule :=
  by
  rintro - ⟨⟨x, hx⟩, hx', rfl⟩
  specialize hq hx'
  rw [Submodule.mem_comap, LinearMap.restrict_apply] at hq
  simpa [hq] using hp hx

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