`BookProof.BrstReducedTransfer.stoneU_mem_physicalStates` (t : ℝ) {x : H} (hx : x ∈ physicalStates Om) : T.stoneU t x ∈ physicalStates Om

Initializing...

`BookProof.BrstReducedTransfer.stoneU_mem_physicalStates` (t : ℝ) {x : H} (hx : x ∈ physicalStates Om) : T.stoneU t x ∈ physicalStates Om · Prove2Me