ofCompleteSpace — Mathlib

English

If K is a complete subspace (closed, hence has a projection in a Hilbert space), there exists an orthogonal projection from E onto K.

Русский

Если K — полное подпространство, то в пространстве Гильберта существует ортогональная проекция из E на K.

LaTeX

$$K.HasOrthogonalProjection exists for complete subspace K in E$$

Lean4

instance (priority := 100) ofCompleteSpace [CompleteSpace K] : K.HasOrthogonalProjection where
  exists_orthogonal
    v :=
    by
    rcases K.exists_norm_eq_iInf_of_complete_subspace (completeSpace_coe_iff_isComplete.mp ‹_›) v with ⟨w, hwK, hw⟩
    refine ⟨w, hwK, (K.mem_orthogonal' _).2 ?_⟩
    rwa [← K.norm_eq_iInf_iff_inner_eq_zero hwK]

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