comp — Mathlib

English

If p is f-invariant and p is g-invariant, then p is invariant under f ∘ g.

Русский

Если p инвариантно относительно f и относительно g, то p инвариантно относительно композиции f ∘ g.

LaTeX

$$$\forall p:\ Submodule R M,\; (p ∈ f.invtSubmodule) \land (p ∈ g.invtSubmodule) \Rightarrow p ∈ invtSubmodule (f \circ_⊙ g)$$$

Lean4

protected theorem comp {p : Submodule R M} {g : End R M} (hf : p ∈ f.invtSubmodule) (hg : p ∈ g.invtSubmodule) :
    p ∈ invtSubmodule (f ∘ₗ g) := fun _ hx ↦ hf (hg hx)

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