instStarHomClassOfLinearMapClassComplexOfOrderHomClass

English

An element p is a star projection iff it is idempotent and normal.

Русский

Элемент p является звездной проекцией тогда и только тогда, когда он идемпотентен и нормален.

LaTeX

$$$$\text{IsStarProjection}(p) \iff (\text{IsIdempotentElem}(p) \wedge \text{IsStarNormal}(p)).$$$$

Lean4

instance {F : Type*} [FunLike F A₁ A₂] [LinearMapClass F ℂ A₁ A₂] [OrderHomClass F A₁ A₂] : StarHomClass F A₁ A₂ where
  map_star f
    a := by
    obtain ⟨y, hy_nonneg, hy_norm, hy⟩ := CStarAlgebra.exists_sum_four_nonneg a
    have hy' : ∀ x : Fin 4, star (y x) = y x := fun x => by rw [IsSelfAdjoint.star_eq (hy_nonneg x).isSelfAdjoint]
    have hy'' : ∀ x : Fin 4, star (f (y x)) = f (y x) := fun x => by
      rw [IsSelfAdjoint.star_eq (map_nonneg f (hy_nonneg x)).isSelfAdjoint]
    simp [hy, hy', hy'']

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