`BookProof.DirectSumEsa.dsCore_dense` (hD : ∀ i, Dense ((D i : Submodule ℂ (G i)) : Set (G i))) : Dense ((dsCore D : Submodule ℂ (lp G 2)) : Set (lp G 2))
ProvedBookProof.DirectSumEsa.dsCore_densetheoremstimepiece
Prove the following Lean 4 theorem from ChapterDirectSumEsa.
BookProof.DirectSumEsa.dsCore_dense (hD : ∀ i, Dense ((D i : Submodule ℂ (G i)) : Set (G i))) : Dense ((dsCore D : Submodule ℂ (lp G 2)) : Set (lp G 2))
Formalization note: Lean 4 identifier BookProof.DirectSumEsa.dsCore_dense.
Preamble
-- Generated from ChapterDirectSumEsa.lean — theorem BookProof.DirectSumEsa.dsCore_dense
import Definitions.Def_ChapterFarisLavine
import Mathlib
import Definitions.Def_ChapterDirectSumEsa
open BookProof.DirectSumEsa
open scoped ENNReal
open BookProof.FarisLavine
noncomputable section
variable {ι : Type*} {G : ι → Type*} [∀ i, NormedAddCommGroup (G i)]
[∀ i, InnerProductSpace ℂ (G i)]
variable {D : ∀ i, Submodule ℂ (G i)}
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]Formal statement
theorem BookProof.DirectSumEsa.dsCore_dense (hD : ∀ i, Dense ((D i : Submodule ℂ (G i)) : Set (G i))) :
Dense ((dsCore D : Submodule ℂ (lp G 2)) : Set (lp G 2)) := by sorry