`BookProof.UnboundedSpectralModel.op_resOp_inc` (T : UnboundedSelfAdjoint H) (y : H) : T.op ⟨resOp T y, resOp_mem T y⟩ = y + Complex.I • resOp T y

Initializing...

`BookProof.UnboundedSpectralModel.op_resOp_inc` (T : UnboundedSelfAdjoint H) (y : H) : T.op ⟨resOp T y, resOp_mem T y⟩ = y + Complex.I • resOp T y · Prove2Me