(S : Submodule ℂ F) (hS : 0 < Module.finrank ℂ S) : ∃ x : F, x ∈ S ∧ ‖x‖ = 1

-- Generated from ChapterSirkRitzMinMax.lean — theorem BookProof.RitzMinMax.exists_unit_mem
import Mathlib
import Definitions.Def_ChapterSirkRitzMinMax
open BookProof.RitzMinMax









noncomputable section


open BookProof.HermiteGalerkin BookProof.ChapterSirkRitzSpectrum
open Filter Topology

variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]

theorem BookProof.RitzMinMax.exists_unit_mem (S : Submodule ℂ F) (hS : 0 < Module.finrank ℂ S) :
    ∃ x : F, x ∈ S ∧ ‖x‖ = 1 := by sorry