isStarProjection_starProjection — Mathlib

English

A star projection is equivalent to a symmetric projection; and this equivalence persists under natural transformations.

Русский

Звёздная проекция эквивалентна симметричной проекции; эта эквивалентность сохраняется под естественными преобразованиями.

LaTeX

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

Lean4

/-- `U.starProjection` is a star projection. -/
@[simp]
theorem isStarProjection_starProjection [CompleteSpace E] {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] :
    IsStarProjection U.starProjection :=
  ⟨U.isIdempotentElem_starProjection, isSelfAdjoint_starProjection U⟩

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