mem_invtSubmodule_iff — Mathlib

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

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