`BookProof.EnergyBandDecomposition.bandPart_of_mem` (hx : x ∈ band E ε k) (f : X → ℂ) : bandPart E ε k f x = f x

Initializing...

`BookProof.EnergyBandDecomposition.bandPart_of_mem` (hx : x ∈ band E ε k) (f : X → ℂ) : bandPart E ε k f x = f x · Prove2Me