English
A projection onto U along its complement V is symmetric if and only if U ⟂ V.
Русский
Проекция на подпространство U вдоль его дополнения V симметрична тогда и только тогда, когда U ⟂ V.
LaTeX
$$$ hUV.projection.IsSymmetric \iff U \perp V $$$
Lean4
/-- A linear projection onto `U` along its complement `V` is symmetric if
and only if `U` and `V` are pairwise orthogonal. -/
theorem _root_.Submodule.IsCompl.projection_isSymmetric_iff {U V : Submodule 𝕜 E} (hUV : IsCompl U V) :
hUV.projection.IsSymmetric ↔ U ⟂ V := by
rw [IsCompl.projection]
refine ⟨fun h u hu v hv => ?_, fun h x y => ?_⟩
·
rw [← Subtype.coe_mk u hu, ← Subtype.coe_mk v hv, ← Submodule.linearProjOfIsCompl_apply_left hUV ⟨u, hu⟩, ←
U.subtype_apply, ← comp_apply, ← h, comp_apply, linearProjOfIsCompl_apply_right hUV ⟨v, hv⟩, map_zero,
inner_zero_left]
· nth_rw 2 [← hUV.projection_add_projection_eq_self x]
nth_rw 1 [← hUV.projection_add_projection_eq_self y]
rw [isOrtho_iff_inner_eq] at h
simp [inner_add_right, inner_add_left, h, inner_eq_zero_symm]
