English
If for all w ∈ K, ⟪u−v, w⟫ = 0, then K.orthogonalProjectionFn(u) = v.
Русский
Если для всех w ∈ K выполняется ⟪u−v, w⟫ = 0, то K.orthogonalProjectionFn(u) = v.
LaTeX
$$$\forall w∈K, \langle u-v, w\rangle = 0 \Rightarrow K.orthogonalProjectionFn(u) = v$$$
Lean4
/-- The unbundled orthogonal projection is the unique point in `K`
with the orthogonality property. This lemma is only intended for use
in setting up the bundled version and should not be used once that is
defined. -/
theorem eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero {u v : E} (hvm : v ∈ K) (hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0) :
K.orthogonalProjectionFn u = v := by
rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜]
have hvs : K.orthogonalProjectionFn u - v ∈ K := Submodule.sub_mem K (orthogonalProjectionFn_mem u) hvm
have huo : ⟪u - K.orthogonalProjectionFn u, K.orthogonalProjectionFn u - v⟫ = 0 :=
orthogonalProjectionFn_inner_eq_zero u _ hvs
have huv : ⟪u - v, K.orthogonalProjectionFn u - v⟫ = 0 := hvo _ hvs
have houv : ⟪u - v - (u - K.orthogonalProjectionFn u), K.orthogonalProjectionFn u - v⟫ = 0 := by
rw [inner_sub_left, huo, huv, sub_zero]
rwa [sub_sub_sub_cancel_left] at houv
