starProjection_comp_starProjection_eq_zero_iff

English

`U.starProjection ∘ L V.starProjection = 0` iff `U` and `V` are pairwise orthogonal.

Русский

Композиция звездной проекции равна нулю тогда и только тогда, когда U и V ортогональны друг другу.

LaTeX

$$$ U.starProjection \circ_L V.starProjection = 0 \iff U \perp V $$$

Lean4

/-- `U.starProjection ∘ V.starProjection = 0` iff `U` and `V` are pairwise orthogonal. -/
theorem starProjection_comp_starProjection_eq_zero_iff {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection]
    [V.HasOrthogonalProjection] : U.starProjection ∘L V.starProjection = 0 ↔ U ⟂ V :=
  by
  refine ⟨fun h => ?_, fun h => h.starProjection_comp_starProjection⟩
  rw [← orthogonalProjection_comp_subtypeL_eq_zero_iff]
  simp only [ContinuousLinearMap.ext_iff, ContinuousLinearMap.comp_apply, subtypeL_apply, starProjection_apply,
    ContinuousLinearMap.zero_apply, coe_eq_zero] at h ⊢
  intro x
  simpa using h (x : E)

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