`BookProof.ReducedEsa.mem_redDom_iff` {x : sector P} : x ∈ redDom P D ↔ (x : F) ∈ D
ProvedBookProof.ReducedEsa.mem_redDom_ifftheoremstimepiece
Prove the following Lean 4 theorem from ChapterReducingSubspaceEsa.
BookProof.ReducedEsa.mem_redDom_iff {x : sector P} : x ∈ redDom P D ↔ (x : F) ∈ D
Formalization note: Lean 4 identifier BookProof.ReducedEsa.mem_redDom_iff.
Preamble
-- Generated from ChapterReducingSubspaceEsa.lean — theorem BookProof.ReducedEsa.mem_redDom_iff
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}Formal statement
theorem BookProof.ReducedEsa.mem_redDom_iff {x : sector P} : x ∈ redDom P D ↔ (x : F) ∈ D := by sorry