ofIsCompl_left_apply — Mathlib

English

From a complement IsCompl p q, and two linear maps φ: p→F, ψ: q→F, construct the global linear map on E by combining φ and ψ on the complementary pieces.

Русский

Из дополняющих подпространств p,q и линейных отображений φ: p→F, ψ: q→F строят глобальное отображение на E, объединяя значения на сумме компонентов.

LaTeX

$$$\text{Given } h:IsCompl(p,q),\; φ,p\to F,\; ψ:q\to F,\; E= p\oplus q:\; ofIsCompl\;h\;φ\ ψ:E→F, \; (a+b)\mapsto φ(a)+ψ(b).$$$

Lean4

@[simp]
theorem ofIsCompl_left_apply (h : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} (u : p) :
    ofIsCompl h φ ψ (u : E) = φ u := by simp [ofIsCompl]

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