Commit 2024-10-13 23:54 cd125921

View on Github →

refactor(Topology/Order/ScottTopology): Unify concepts of Scott Topology (#16523) Unify Scott Topologies, following on from #13201 and #16826. Originally Mathlib had a notion of ω-Scott Continuity and ω-Scott Topology based on Chains for ω-complete partial orders. Previously we introduced a notion of Scott Continuity and Scott Topology based on directed sets for arbitrary pre-orders (#2508). In #13201, we generalised our definition of Scott Continuity to include ω-Scott Continuity as a special case. This PR continues that work by generalising our notion of Scott Topology to include ω-Scott Topology as a special case. Topology.IsScott.scottContinuous_iff_continuous and Topology.IsScott.ωscottContinuous_iff_continuous have almost identical proofs and are presumably special cases of a more general result that I have not yet formulated. However I think this PR covers enough ground to be worth considering at this stage.

Estimated changes

Modified Mathlib/Topology/OmegaCompletePartialOrder.lean

added theorem Topology.IsScott.ωscottContinuous_iff_continuous

added theorem isOpen_iff_ωScottContinuous_mem

added theorem scott_eq_Scott

Modified Mathlib/Topology/Order/LawsonTopology.lean

modified def Topology.IsLawson.lawsonBasis

modified def Topology.lawson

modified theorem Topology.lawson_le_scott

modified theorem Topology.scottHausdorff_le_isLawson

modified theorem Topology.scottHausdorff_le_lawson

Modified Mathlib/Topology/Order/ScottTopology.lean

added theorem DirSupInacc.dirSupInaccOn

added theorem DirSupInaccOn.mono

added def DirSupInaccOn

modified theorem Topology.IsLower.scottHausdorff_le

modified theorem Topology.IsScott.closure_singleton

modified theorem Topology.IsScott.dirSupClosed_of_isClosed

modified theorem Topology.IsScott.isClosed_Iic

modified theorem Topology.IsScott.isClosed_iff_isLowerSet_and_dirSupClosed

modified theorem Topology.IsScott.isLowerSet_of_isClosed

modified theorem Topology.IsScott.isOpen_iff_Iic_compl_or_univ

deleted theorem Topology.IsScott.isOpen_iff_isUpperSet_and_dirSupInacc

added theorem Topology.IsScott.isOpen_iff_isUpperSet_and_dirSupInaccOn

modified theorem Topology.IsScott.isOpen_iff_isUpperSet_and_scottHausdorff_open

modified theorem Topology.IsScott.isOpen_iff_scottContinuous_mem

modified theorem Topology.IsScott.isUpperSet_of_isOpen

modified theorem Topology.IsScott.lowerClosure_subset_closure

modified theorem Topology.IsScott.monotone_of_continuous

modified theorem Topology.IsScott.scottContinuous_iff_continuous

modified theorem Topology.IsScott.scottHausdorff_le

modified theorem Topology.IsScott.scott_eq_upper_of_completeLinearOrder

modified theorem Topology.IsScott.topology_eq

modified def Topology.IsScott.withScottHomeomorph

modified theorem Topology.IsScottHausdorff.dirSupClosed_of_isClosed

added theorem Topology.IsScottHausdorff.dirSupInaccOn_of_isOpen

deleted theorem Topology.IsScottHausdorff.dirSupInacc_of_isOpen

modified theorem Topology.IsScottHausdorff.isOpen_iff

modified theorem Topology.IsScottHausdorff.topology_eq

modified def Topology.scott

modified def Topology.scottHausdorff

modified theorem Topology.scottHausdorff_le_lower

modified theorem Topology.scottHausdorff_le_scott

modified theorem Topology.upperSet_le_scott

added theorem dirSupInaccOn_univ