Commit 2023-09-15 08:07 b0e5bef3

View on Github →

feat(Order/OmegaCompletePartialOrder): Show that Scott Continuity implies OmegaCompletePartialOrder.Continuous' (#6831) In https://github.com/leanprover-community/mathlib/pull/18517 we introduced the notion of a Scott Continuous function between preorders. This PR shows that a Scott Continuous function between OmegaCompletePartialOrders is necessarily OmegaCompletePartialOrder.Continuous'.

Estimated changes

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

added theorem OmegaCompletePartialOrder.IsLUB_of_ScottContinuous

added theorem OmegaCompletePartialOrder.IsLUB_range_ωSup

added theorem OmegaCompletePartialOrder.ScottContinuous.continuous'

added theorem OmegaCompletePartialOrder.ωSup_eq_of_IsLUB