Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-03-26 20:12
2f26d1a1
View on Github →
feat: characterization of open/closed sets in Scott-Hausdorff topology (
#37227
)
Estimated changes
Modified
Mathlib/Topology/Order/ScottTopology.lean
added
theorem
Topology.IsScottHausdorff.isClosed_iff_dirSupClosed
added
theorem
Topology.IsScottHausdorff.isOpen_iff_dirSupInacc