isStarProjection_iff_isSymmetricProjection

English

A linear map is a star projection iff it is a symmetric projection.

Русский

Линейное отображение является звездной проекцией тогда и только тогда, когда оно симметричная проекция.

LaTeX

$$$$\text{IsStarProjection}(T) \iff T.IsSymmetricProjection.$$$$

Lean4

theorem isStarProjection_iff_isSymmetricProjection {T : E →ₗ[𝕜] E} : IsStarProjection T ↔ T.IsSymmetricProjection := by
  simp [← isStarProjection_toContinuousLinearMap_iff, ContinuousLinearMap.isStarProjection_iff_isSymmetricProjection]

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