English
For p ⊆ E and a projection defined via IsCompl, applying the projection to i x (where i is the injection used to define the projection) yields x.
Русский
Пусть задаётся проекция через IsCompl; применение проекции к i x возвращает x.
LaTeX
$$$\text{If } i:F\to E\text{ and } x\in F,\; (\mathrm{linearProjOfIsCompl}\; q\; i\; hi\; h)(i x)=x.$$$
Lean4
@[simp]
theorem linearProjOfIsCompl_apply_left {F : Type*} [AddCommGroup F] [Module R F] (i : F →ₗ[R] E)
(hi : Function.Injective i) (h : IsCompl (LinearMap.range i) q) (x : F) : linearProjOfIsCompl q i hi h (i x) = x :=
by
let ix : LinearMap.range i := ⟨i x, mem_range_self i x⟩
change linearProjOfIsCompl q i hi h ix = x
rw [linearProjOfIsCompl, coe_comp, LinearEquiv.coe_coe, Function.comp_apply, LinearEquiv.symm_apply_eq,
Submodule.linearProjOfIsCompl_apply_left, Subtype.ext_iff, LinearEquiv.ofInjective_apply]
