starProjection_mem_subspace_eq_self

English

Let f be a linear isometry between E and E' and K ⊆ E with HasOrthogonalProjection. Then f(P_K(x)) = P_{f(K)}(f(x)) for all x ∈ E.

Русский

Пусть f — линейная изометрия между E и E', K ⊆ E имеет ортогональную проекцию. Тогда для всех x ∈ E выполняется f(P_K(x)) = P_{f(K)}(f(x)).

LaTeX

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

Lean4

@[simp]
theorem starProjection_mem_subspace_eq_self (v : K) : K.starProjection v = v := by simp [starProjection_apply]

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