The Lean 4 theorem `finiteModeDomain_eq_iSup` in the `ChapterHermiteGalerkinFriedrichs` chapter of the timepiece formalization
ProvedBookProof.HermiteGalerkin.finiteModeDomain_eq_iSuptimepiece
The Lean 4 theorem finiteModeDomain_eq_iSup in the ChapterHermiteGalerkinFriedrichs chapter of the timepiece formalization.
Preamble
-- Generated from ChapterHermiteGalerkinFriedrichs.lean — theorem BookProof.HermiteGalerkin.finiteModeDomain_eq_iSup
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.finiteModeDomain_eq_iSup (b : HilbertBasis ℕ ℂ F) :
finiteModeDomain b = ⨆ m : ℕ, galerkinSpan b m := by sorrySource