The Lean 4 theorem `exists_mem_galerkinSpan` in the `ChapterHermiteGalerkinFriedrichs` chapter of the timepiece formalization
ProvedBookProof.HermiteGalerkin.exists_mem_galerkinSpantimepiece
The Lean 4 theorem exists_mem_galerkinSpan in the ChapterHermiteGalerkinFriedrichs chapter of the timepiece formalization.
Preamble
-- Generated from ChapterHermiteGalerkinFriedrichs.lean — theorem BookProof.HermiteGalerkin.exists_mem_galerkinSpan
import Mathlib
import Definitions.Def_ChapterHermiteGalerkinFriedrichs
open BookProof.HermiteGalerkin
open BookProof.FarisLavine BookProof.YangMillsFriedrichs BookProof.YangMillsFriedrichsLimit
open Filter Topology
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]Formal statement
theorem BookProof.HermiteGalerkin.exists_mem_galerkinSpan (b : HilbertBasis ℕ ℂ F) {x : F} (hx : x ∈ finiteModeDomain b) :
∃ m : ℕ, x ∈ galerkinSpan b m := by sorrySource