ofIsCompl_right_apply — Mathlib

English

In the IsCompl decomposition, the right projection applied to a vector of q yields its component in q.

Русский

В разложении IsCompl правая проекция возвращает компоненту в q.

LaTeX

$$$\text{If } v\in q,\; (\mathrm{ofIsCompl}\ h\ φ\ ψ)(v)=ψ(v).$$$

Lean4

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

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