orthogonalProjection_comp_subtypeL_eq_zero_iff

English

The projection from U to V is zero iff U and V are orthogonal.

Русский

Проекция from U onto V равна нулю тогда и только тогда, когда U и V ортогональны.

LaTeX

$$$ U.orthogonalProjection \circ_L V.subtypeL = 0 \iff U \perp V $$$

Lean4

/-- The projection into `U` from `V` is the zero map if and only if `U` and `V` are orthogonal. -/
theorem orthogonalProjection_comp_subtypeL_eq_zero_iff {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] :
    U.orthogonalProjection ∘L V.subtypeL = 0 ↔ U ⟂ V :=
  ⟨fun h u hu v hv => by
    convert starProjection_inner_eq_zero v u hu using 2
    have : U.orthogonalProjection v = 0 := DFunLike.congr_fun h (⟨_, hv⟩ : V)
    rw [starProjection_apply, this, Submodule.coe_zero, sub_zero], Submodule.IsOrtho.orthogonalProjection_comp_subtypeL⟩

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