Core-compact+well-filtered T0=sober locally compact

Last time, I motivated the construction of the well-filterification Wf(X) of a space X of X. Xu, Ch. Shen, X. Xi and D. Zhao by saying that it was needed to understand their proof of the fact that every core-compact well-filtered T₀ space is sober, and hence also locally compact. This solves a question asked by X. Jia, and first solved positively by J. Lawson and X. Xi. I then realized that their proof contains a (somewhat concealed) gem; polishing it reveals an interesting new variant of the Hofmann-Mislove theorem, which applies to well-filtered spaces rather than to sober spaces, and rests on a funny countability assumption. We will see that the latter is satisfied in all core-compact spaces, and this will allow us to show that all core-compact well-filtered T₀ spaces are locally compact, hence sober. Read the full post.