English
If p and q are complementary, then there is a single linear map on E determined by its restrictions to p and q; equivalently, the map is uniquely determined by φ: p→F and ψ: q→F with compatibility on E.
Русский
Если p и q комплементны, существует единственная линейная карта на E, задаваемая своими ограничениями на p и q; и карта определяется единственным образом при задании φ: p→F и ψ: q→F с совместимостью на E.
LaTeX
$$$\text{If } h:IsCompl(p,q),\; φ:p→F,\; ψ:q→F,\; χ:E→F,\; φ|_{p}=χ|_{p},\; ψ|_{q}=χ|_{q},\;\text{then } ofIsCompl\;h\;φ\ ψ = χ.$$$
Lean4
/-- Given linear maps `φ` and `ψ` from complement submodules, `LinearMap.ofIsCompl` is
the induced linear map over the entire module. -/
def ofIsCompl {p q : Submodule R E} (h : IsCompl p q) (φ : p →ₗ[R] F) (ψ : q →ₗ[R] F) : E →ₗ[R] F :=
LinearMap.coprod φ ψ ∘ₗ ↑(Submodule.prodEquivOfIsCompl _ _ h).symm
