English
The glued map equals the sum of two projections against the IsCompl decomposition: ofIsCompl h φ ψ = φ ∘ p.linearProjOfIsCompl q hpq + ψ ∘ q.linearProjOfIsCompl p hpq.symm.
Русский
Слитое отображение равно сумме проекций по разложению IsCompl: ofIsCompl h φ ψ = φ ∘ p.linearProjOfIsCompl q hpq + ψ ∘ q.linearProjOfIsCompl p hpq.symm.
LaTeX
$$$\mathrm{ofIsCompl}\;h\;φ\ ψ = (φ \circ p.linearProjOfIsCompl\ q\ hpq) + (ψ \circ q.linearProjOfIsCompl\ p\ hpq.symm).$$$
Lean4
theorem ofIsCompl_eq_add (hpq : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} :
ofIsCompl hpq φ ψ = (φ ∘ₗ p.linearProjOfIsCompl q hpq) + (ψ ∘ₗ q.linearProjOfIsCompl p hpq.symm) :=
by
ext x
obtain ⟨a, b, rfl, _⟩ := existsUnique_add_of_isCompl hpq x
simp
