exists_add_mem_mem_orthogonal — Mathlib

English

The star projection of an element of K onto Kᗮ is zero.

Русский

Звёздная проекция элемента K на Kᗮ равна нулю.

LaTeX

$$$ K^{\perp}.starProjection(v) = 0 \quad \text{если } v \in K $$$

Lean4

/-- If `K` is complete, any `v` in `E` can be expressed as a sum of elements of `K` and `Kᗮ`. -/
theorem exists_add_mem_mem_orthogonal [K.HasOrthogonalProjection] (v : E) : ∃ y ∈ K, ∃ z ∈ Kᗮ, v = y + z :=
  ⟨K.orthogonalProjection v, Subtype.coe_prop _, v - K.orthogonalProjection v, sub_starProjection_mem_orthogonal _, by
    simp⟩

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