`BookProof.TensorCore.graphPow_tmul_mem_closure` (hcore : IsGraphCore D A) (n : ℕ) (ih : ∀ b : ((domSpace Hs D₂).pow n), graphPow Hs D₂ A n b ∈ (Submodule.map (graphPow Hs D₂ A n)

Proved

BookProof.TensorCore.graphPow_tmul_mem_closure

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterTensorGraphCore.

BookProof.TensorCore.graphPow_tmul_mem_closure (hcore : IsGraphCore D A) (n : ℕ) (ih : ∀ b : ((domSpace Hs D₂).pow n), graphPow Hs D₂ A n b ∈ (Submodule.map (graphPow Hs D₂ A n) (corePow Hs D₂ D n)).topologicalClosure) (a : D₂) (b : ((domSpace Hs D₂).pow n)) : graphPow Hs D₂ A (n + 1) (a ⊗ₜ[ℂ] b) ∈ (Submodule.map (graphPow Hs D₂ A (n + 1)) (corePow Hs D₂ D (n + 1))).topologicalClosure

Formalization note: Lean 4 identifier BookProof.TensorCore.graphPow_tmul_mem_closure.

Preamble

-- Generated from ChapterTensorGraphCore.lean — theorem BookProof.TensorCore.graphPow_tmul_mem_closure
import Definitions.Def_ChapterFarisLavine
import Mathlib
import Definitions.Def_ChapterTensorGraphCore
import Definitions.Def_ChapterGraphCoreTransfer
open BookProof.GraphCore
open BookProof.TensorCore



open scoped TensorProduct
open BookProof.FarisLavine BookProof.GraphCore

noncomputable section

variable (Hs : IPSpace) (D₂ : Submodule ℂ Hs.carrier)
variable (A : D₂ →ₗ[ℂ] Hs.carrier)
variable (D : Submodule ℂ Hs.carrier)

Formal statement

theorem BookProof.TensorCore.graphPow_tmul_mem_closure (hcore : IsGraphCore D A) (n : ℕ)
    (ih : ∀ b : ((domSpace Hs D₂).pow n), graphPow Hs D₂ A n b ∈
      (Submodule.map (graphPow Hs D₂ A n) (corePow Hs D₂ D n)).topologicalClosure)
    (a : D₂) (b : ((domSpace Hs D₂).pow n)) :
    graphPow Hs D₂ A (n + 1) (a ⊗ₜ[ℂ] b) ∈
      (Submodule.map (graphPow Hs D₂ A (n + 1))
        (corePow Hs D₂ D (n + 1))).topologicalClosure := by sorry

View graph