Commit 2023-02-03 07:53 7bfd7d10

View on Github →

feat: port Topology.OmegaCompletePartialOrder (#2034)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/OmegaCompletePartialOrder.lean

added theorem Scott.IsOpen.inter

added def Scott.IsOpen

added def Scott.IsωSup

added theorem Scott.isOpen_unionₛ

added theorem Scott.isOpen_univ

added theorem Scott.isωSup_iff_isLUB

added def Scott

added theorem continuous_of_scottContinuous

added theorem isωSup_ωSup

added def notBelow

added theorem notBelow_isOpen

added theorem scottContinuous_of_continuous