English
There is a canonical linear projection from E onto p along q that sends each x ∈ E to its p-component in the unique decomposition x = u + v with u ∈ p, v ∈ q.
Русский
Существует каноническая линейная проекция из E на p вдоль q, отправляющая каждое x ∈ E в его p-компоненту в единственном разложении x = u + v, где u ∈ p, v ∈ q.
LaTeX
$$$\exists!\ f: E \to p\text{ линейная},\; x = u+v\,(u\in p, v\in q) \Rightarrow f(x)=u$$$
Lean4
/-- Projection to a submodule along a complement. It is the unique
linear map `f : E → p` such that `f x = x` for `x ∈ p` and `f x = 0` for `x ∈ q`.
See also `LinearMap.linearProjOfIsCompl`. -/
def linearProjOfIsCompl (h : IsCompl p q) : E →ₗ[R] p :=
LinearMap.fst R p q ∘ₗ ↑(prodEquivOfIsCompl p q h).symm
