less unpacked proof characterizing P -> Q when P closed, Q open

[ecavallo]

I don't know which style you prefer.
It's also only necessary that $\lnot P$ is open, not that $P$ is closed, but I don't know whether this is useful.

[felixwellen]

I prefer this proof and I think it makes sense to state it in the extra generality, that it is enough if $\neg P$ is open. One example of such a proposition $P$, which is not closed, would be $P(x):\equiv \neg\neg(x=0)$ for $x\in R$.