isStarProjection_toContinuousLinearMap_iff

English

A map is a star projection iff its associated continuous linear map is a star projection.

Русский

Отображение является звездной проекцией тогда и только тогда, когда соответствующее непрерывное линейное отображение тоже звездная проекция.

LaTeX

$$$$\text{IsStarProjection}(T) \iff \text{IsStarProjection}(T^{\toContinuousLinearMap}).$$$$

Lean4

theorem isStarProjection_toContinuousLinearMap_iff {T : E →ₗ[𝕜] E} :
    have := FiniteDimensional.complete 𝕜 E
    IsStarProjection (toContinuousLinearMap T) ↔ IsStarProjection T :=
  by
  simp [isStarProjection_iff, isSelfAdjoint_toContinuousLinearMap_iff,
    ← ContinuousLinearMap.isIdempotentElem_toLinearMap_iff]

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