Compact closed subsets in the patch topology

Given a coherent, well-filtered space X, one can give a pretty explicit description of the compact closed sets in X^patch, the space obtained by equipping X with its patch topology—and we do not need local compactness or compactness. They are exactly the non-empty intersections of finite unions of lenses. This wonderful result lies somewhere in a paper on measure extension theorems for T₀ space of Klaus Keimel and Jimmie Lawson, and has a very clever proof, which J. Lawson sent me recently. Read the full post.