Commit 2026-05-11 12:09 3a72b0fe

View on Github →

feat: generalize isOpen_iff_dirSupInacc (#37307) Under mild conditions (D being a lower set is sufficient though not necessary), open and closed sets in the ScottHausdorff D topology correspond to DirSupInaccOn D and DirSupClosedOn D sets.

Estimated changes

Modified Mathlib/Order/DirSupClosed.lean

Modified Mathlib/Topology/Order/ScottTopology.lean

modified theorem Topology.IsLower.scottHausdorff_le

added theorem Topology.IsScottHausdorff.dirSupClosedOn_of_isClosed

deleted theorem Topology.IsScottHausdorff.dirSupClosed_of_isClosed

modified theorem Topology.IsScottHausdorff.dirSupInaccOn_of_isOpen

modified theorem Topology.IsScottHausdorff.isClosed_iff_dirSupClosed

added theorem Topology.IsScottHausdorff.isClosed_iff_dirSupClosedOn

modified theorem Topology.IsScottHausdorff.isClosed_of_isUpperSet

modified theorem Topology.IsScottHausdorff.isOpen_iff

modified theorem Topology.IsScottHausdorff.isOpen_iff_dirSupInacc

added theorem Topology.IsScottHausdorff.isOpen_iff_dirSupInaccOn

modified theorem Topology.IsScottHausdorff.isOpen_of_isLowerSet

modified theorem Topology.IsScottHausdorff.topology_eq