: (fockCore fiberCore : Submodule ℂ (lp fiberSector 2)) ≠ ⊤
ProvedBookProof.NavierStokesFlow.SecondQuant.fockComparison_domain_ne_topnavier-stokesoperator-algebrastimepiece
Lean 4 theorem BookProof.NavierStokesFlow.SecondQuant.fockComparison_domain_ne_top (module BookProof.NavierStokesFlow), source chapter BookProof/ChapterNavierStokesFlow.lean.
Preamble
-- Generated from ChapterNavierStokesFockFarisLavine.lean — theorem BookProof.NavierStokesFlow.SecondQuant.fockComparison_domain_ne_top
import Mathlib
import Definitions.Def_ChapterNavierStokesFockFarisLavine
open BookProof.NavierStokesFlow
open BookProof.NavierStokesFlow.SecondQuant
open scoped ENNReal
open FarisLavineLift
variable {ι : Type*}
variable {S : ι → Type*} [∀ m, NormedAddCommGroup (S m)] [∀ m, InnerProductSpace ℂ (S m)]
variable {D : ∀ m, Submodule ℂ (S m)}
open FarisLavineLift LpNat DiagonalEsaFormal statement
theorem BookProof.NavierStokesFlow.SecondQuant.fockComparison_domain_ne_top :
(fockCore fiberCore : Submodule ℂ (lp fiberSector 2)) ≠ ⊤ := by sorrySource