English
The projection associated with a complement is the unique linear map E → p that sends p to itself and kills q.
Русский
Связанная с комплементом проекция является единственной линейной картой E → p, которая отправляет p в себя и выкидывает q в ноль.
LaTeX
$$$\text{There exists a unique } f: E \to p \text{ s.t. } f|_p = \mathrm{id}_p \text{ and } f|_q = 0$$$
Lean4
/-- The linear projection onto a subspace along its complement
as a map from the full space to itself, as opposed to `Submodule.linearProjOfIsCompl`,
which maps into the subtype.
This version is important as it satisfies `IsIdempotentElem`. -/
noncomputable def projection (hpq : IsCompl p q) :=
p.subtype ∘ₗ p.linearProjOfIsCompl q hpq
