`BookProof.GraphCore.mem_pushDom` (U : F →ₗᵢ[ℂ] G) {D : Submodule ℂ F} (x : D) : U (x : F) ∈ pushDom U D

Proved

BookProof.GraphCore.mem_pushDom

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterGraphCoreTransfer.

BookProof.GraphCore.mem_pushDom (U : F →ₗᵢ[ℂ] G) {D : Submodule ℂ F} (x : D) : U (x : F) ∈ pushDom U D

Formalization note: Lean 4 identifier BookProof.GraphCore.mem_pushDom.

Preamble

-- Generated from ChapterGraphCoreTransfer.lean — theorem BookProof.GraphCore.mem_pushDom
import Definitions.Def_ChapterFarisLavine
import Mathlib
import Definitions.Def_ChapterGraphCoreTransfer
open BookProof.GraphCore



open BookProof.FarisLavine

variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]

variable {G : Type*} [NormedAddCommGroup G] [InnerProductSpace ℂ G]

Formal statement

theorem BookProof.GraphCore.mem_pushDom (U : F →ₗᵢ[ℂ] G) {D : Submodule ℂ F} (x : D) :
    U (x : F) ∈ pushDom U D := by sorry

View graph