starProjection_comp_starProjection

English

For orthogonal subspaces U and V, the composition U.starProjection ∘ L V.starProjection equals zero when U ⟂ V.

Русский

Для ортогональных подпространств U и V композиция U.starProjection и V.starProjection равна нулю, если U ⟂ V.

LaTeX

$$$ U.starProjection \circ_L V.starProjection = 0 \quad \text{если } U \perp V $$$

Lean4

theorem starProjection_comp_starProjection {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] [V.HasOrthogonalProjection]
    (h : U ⟂ V) : U.starProjection ∘L V.starProjection = 0 :=
  calc
    _ = U.subtypeL ∘L (U.orthogonalProjection ∘L V.subtypeL) ∘L V.orthogonalProjection := by
      simp only [starProjection, ContinuousLinearMap.comp_assoc]
    _ = 0 := by simp [h.orthogonalProjection_comp_subtypeL]

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