sub_starProjection_mem_orthogonal

English

For any v in E, the difference v − P_K v lies in the orthogonal complement K^⊥.

Русский

Для любого v ∈ E разность v − P_K v принадлежит ортогональному дополнению K^⊥.

LaTeX

$$$v - P_K(v) \in K^{\perp}$$$

Lean4

/-- The difference of `v` from its orthogonal projection onto `K` is in `Kᗮ`. -/
@[simp]
theorem sub_starProjection_mem_orthogonal (v : E) : v - K.starProjection v ∈ Kᗮ :=
  by
  intro w hw
  rw [inner_eq_zero_symm]
  exact starProjection_inner_eq_zero _ _ hw

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