orthogonalProjection_mem_subspace_eq_self

English

For any subspace U with an orthogonal projection, P_{U^⊥} = I − P_U.

Русский

Для любого подпространства U с ортогональной проекцией: P_{U^⊥} = I − P_U.

LaTeX

$$P_{U^{\perp}} = \mathrm{Id} - P_U.$$

Lean4

/-- The orthogonal projection sends elements of `K` to themselves. -/
@[simp]
theorem orthogonalProjection_mem_subspace_eq_self (v : K) : K.orthogonalProjection v = v :=
  by
  ext
  apply eq_starProjection_of_mem_of_inner_eq_zero <;> simp

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