Commit 2024-09-17 11:41 9a321de8

feat(Topology/Order): Sierpiński space classifies open sets of Scott topology (#16826) This PR shows that the Sierpiński topology coincides with the upper topology on Prop, and hence with the Scott topology (since Prop is a complete linear order). This observation reveals that a subset of a preorder is open in the Scott topology if and only if its characteristic function is Scott continuous.