`BookProof.ReducedEsa.symProj_mem` (hUD : ∀ x ∈ D, U x ∈ D) : ∀ x ∈ D, symProj U x ∈ D
ProvedBookProof.ReducedEsa.symProj_memtheoremstimepiece
Prove the following Lean 4 theorem from ChapterReducingSubspaceEsa.
BookProof.ReducedEsa.symProj_mem (hUD : ∀ x ∈ D, U x ∈ D) : ∀ x ∈ D, symProj U x ∈ D
Formalization note: Lean 4 identifier BookProof.ReducedEsa.symProj_mem.
Preamble
-- Generated from ChapterReducingSubspaceEsa.lean — theorem BookProof.ReducedEsa.symProj_mem
import Definitions.Def_ChapterFarisLavine
import Definitions.Def_ChapterGraphCoreTransfer
import Mathlib
import Definitions.Def_ChapterReducingSubspaceEsa
open BookProof.ReducedEsa
open BookProof.FarisLavine BookProof.GraphCore
noncomputable section
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]
variable {P : F →ₗ[ℂ] F}
variable {D : Submodule ℂ F}
variable (T : D →ₗ[ℂ] F)
variable {T}
variable (U : F →ₗ[ℂ] F)
variable {U}Formal statement
theorem BookProof.ReducedEsa.symProj_mem (hUD : ∀ x ∈ D, U x ∈ D) : ∀ x ∈ D, symProj U x ∈ D := by sorry