English
Let q be an idempotent linear operator on a module M and p : E → M be a linear map. Then q ∘ p = p if and only if the image of p is contained in the image of q.
Русский
Пусть q — идемпотентный линейный оператор на модуле M, и p : E → M — линейный отображение. Тогда q ∘ p = p тогда и только тогда, когда образ p содержится в образе q.
LaTeX
$$$ q \circ p = p \iff \operatorname{Im}(p) \subseteq \operatorname{Im}(q) $$$
Lean4
/-- Given an idempotent linear operator `q`,
we have `q ∘ p = p` iff `range p ⊆ range q` for all `p`. -/
theorem comp_eq_right_iff {q : M →ₗ[S] M} (hq : IsIdempotentElem q) {E : Type*} [AddCommMonoid E] [Module S E]
(p : E →ₗ[S] M) : q.comp p = p ↔ range p ≤ range q := by
simp_rw [LinearMap.ext_iff, comp_apply, ← hq.mem_range_iff, SetLike.le_def, mem_range, forall_exists_index,
forall_apply_eq_imp_iff]
