`BookProof.DirectSumEsa.single_mem_dsCore` [DecidableEq ι] (i : ι) (u : D i) : (lp.single 2 i ((u : G i)) : lp G 2) ∈ dsCore D

Proved

BookProof.DirectSumEsa.single_mem_dsCore

by leonardopedro · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterDirectSumEsa.

BookProof.DirectSumEsa.single_mem_dsCore [DecidableEq ι] (i : ι) (u : D i) : (lp.single 2 i ((u : G i)) : lp G 2) ∈ dsCore D

Formalization note: Lean 4 identifier BookProof.DirectSumEsa.single_mem_dsCore.

Preamble

-- Generated from ChapterDirectSumEsa.lean — theorem BookProof.DirectSumEsa.single_mem_dsCore
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)}

Formal statement

theorem BookProof.DirectSumEsa.single_mem_dsCore [DecidableEq ι] (i : ι) (u : D i) :
    (lp.single 2 i ((u : G i)) : lp G 2) ∈ dsCore D := by sorry

View graph