English
If U is a projection with endomorphism f, then U is invariant under T if and only if f ∘ T ∘ f = T ∘ f.
Русский
Если U является образующим подпространством проекции f, тогда U инвариантно относительно T тогда и только тогда, когда f ∘ T ∘ f = T ∘ f.
LaTeX
$$$ U \in \operatorname{End}_{\!\!\!} \text{invtSubmodule}_T \iff f \circ T \circ f = T \circ f$$$
Lean4
theorem _root_.LinearMap.IsProj.mem_invtSubmodule_iff {U : Submodule R E} (hf : IsProj U f) :
U ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = T ∘ₗ f :=
hf.range ▸ hf.isIdempotentElem.range_mem_invtSubmodule_iff