isStarProjection_iff_isIdempotentElem_and_isStarNormal

English

A star-normal operator T satisfies the norm equality ∥T v∥ = ∥adjoint T v∥ for all v.

Русский

Оператор T нормален по звёздочке тогда и только тогда, когда для всех v выполняется ∥Tv∥ = ∥T* v∥.

LaTeX

$$$\\text{IsStarNormal}(T) \\iff \\forall v, \\|T v\\| = \\|\\operatorname{adjoint}(T) v\\|$$$

Lean4

/-- A continuous linear map is a star projection iff it is idempotent and normal. -/
theorem isStarProjection_iff_isIdempotentElem_and_isStarNormal :
    IsStarProjection T ↔ IsIdempotentElem T ∧ IsStarNormal T :=
  by
  rw [isStarProjection_iff, and_congr_right_iff]
  exact fun h => IsIdempotentElem.isSelfAdjoint_iff_isStarNormal h

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