English
For a linear isometry L and a subspace S, the extension L.extend agrees with L on S.
Русский
Расширение линейного изометрии L совпадает с L на подпространстве S.
LaTeX
$$L.extend s = L s$$
Lean4
theorem extend_apply (L : S →ₗᵢ[𝕜] V) (s : S) : L.extend s = L s :=
by
haveI : CompleteSpace S := FiniteDimensional.complete 𝕜 S
simp only [LinearIsometry.extend, ← LinearIsometry.coe_toLinearMap]
simp only [add_eq_left, LinearIsometry.coe_toLinearMap, LinearIsometryEquiv.coe_toLinearIsometry,
LinearIsometry.coe_comp, Function.comp_apply, orthogonalProjection_mem_subspace_eq_self, LinearMap.coe_comp,
ContinuousLinearMap.coe_coe, Submodule.coe_subtype, LinearMap.add_apply, Submodule.coe_eq_zero,
LinearIsometryEquiv.map_eq_zero_iff, Submodule.coe_subtypeₗᵢ,
orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, Submodule.orthogonal_orthogonal, Submodule.coe_mem]
