isIdempotentElem_starProjection — Mathlib

English

Let f be a linear isometry; then map_starProjection equality expresses how star projections transfer under f.

Русский

Пусть f — линейная изометрия; тогда равенство map_starProjection описывает перенос звездной проекции через f.

LaTeX

$$f (P_K(x)) = P_{f(K)}(f(x))$$

Lean4

@[simp]
theorem isIdempotentElem_starProjection : IsIdempotentElem K.starProjection :=
  ContinuousLinearMap.ext fun x ↦ starProjection_eq_self_iff.mpr <| by simp

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