Commit 2024-09-05 07:28 d6ca7ae2

View on Github →

refactor(Order/OmegaCompletePartialOrder): Unify concepts of Scott Continuity (#13201) We currently have two related but different concepts of Scott Continuity in Mathlib - ScottContinuous in Order/Bounds/Basic and OmegaCompletePartialOrder.Continuous' in Order/OmegaCompletePartialOrder. We previously showed (#6831) that ScottContinuous implies OmegaCompletePartialOrder.Continuous' (in general the converse isn't true). This PR gives a more general definition of Scott Continuity, ScottContinuousOn which specialises to ScottContinuous and something equivalent to OmegaCompletePartialOrder.Continuous' to give a more satisfactory unification of the concepts.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Control/LawfulFix.lean

added theorem Part.fix_eq_of_ωScottContinuous

added theorem Part.fix_eq_ωSup_of_ωScottContinuous

added theorem Part.ωScottContinuous_toUnitMono

modified theorem Pi.uncurry_curry_continuous

added theorem Pi.uncurry_curry_ωScottContinuous

added theorem Pi.ωScottContinuous_curry

added theorem Pi.ωScottContinuous_uncurry

Modified Mathlib/LinearAlgebra/Span.lean

Modified Mathlib/Order/Bounds/Basic.lean

deleted def ScottContinuous

Modified Mathlib/Order/Category/OmegaCompletePartialOrder.lean

Modified Mathlib/Order/Directed.lean

Modified Mathlib/Order/FixedPoints.lean

modified theorem fixedPoints.gfp_eq_sInf_iterate

modified theorem fixedPoints.lfp_eq_sSup_iterate

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

added theorem CompleteLattice.ωScottContinuous.bot

added theorem CompleteLattice.ωScottContinuous.iSup

added theorem CompleteLattice.ωScottContinuous.inf

added theorem CompleteLattice.ωScottContinuous.prodMk

added theorem CompleteLattice.ωScottContinuous.sSup

added theorem CompleteLattice.ωScottContinuous.sup

added theorem CompleteLattice.ωScottContinuous.top

added def OmegaCompletePartialOrder.Chain.pair

added theorem OmegaCompletePartialOrder.Chain.pair_succ

added theorem OmegaCompletePartialOrder.Chain.pair_zero

added theorem OmegaCompletePartialOrder.Chain.pair_zip_pair

added theorem OmegaCompletePartialOrder.Chain.range_pair

modified theorem OmegaCompletePartialOrder.ContinuousHom.coe_mk

modified def OmegaCompletePartialOrder.ContinuousHom.comp

modified theorem OmegaCompletePartialOrder.ContinuousHom.comp_assoc

modified def OmegaCompletePartialOrder.ContinuousHom.const

modified def OmegaCompletePartialOrder.ContinuousHom.id

added theorem OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.bind

added theorem OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.map

added theorem OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.seq

added theorem OmegaCompletePartialOrder.flip₁_continuous'

added theorem OmegaCompletePartialOrder.flip₂_continuous'

added theorem OmegaCompletePartialOrder.ωScottContinuous.apply₂

added theorem OmegaCompletePartialOrder.ωScottContinuous.comp

added theorem OmegaCompletePartialOrder.ωScottContinuous.const

added theorem OmegaCompletePartialOrder.ωScottContinuous.id

added theorem OmegaCompletePartialOrder.ωScottContinuous.isLUB

added theorem OmegaCompletePartialOrder.ωScottContinuous.map_ωSup

added theorem OmegaCompletePartialOrder.ωScottContinuous.monotone

added theorem OmegaCompletePartialOrder.ωScottContinuous.of_apply₂

added def OmegaCompletePartialOrder.ωScottContinuous

added theorem OmegaCompletePartialOrder.ωScottContinuous_iff_apply₂

added theorem OmegaCompletePartialOrder.ωScottContinuous_iff_map_ωSup_of_orderHom

added theorem OmegaCompletePartialOrder.ωScottContinuous_iff_monotone_map_ωSup

modified theorem OmegaCompletePartialOrder.ωSup_le_iff

deleted theorem Pi.OmegaCompletePartialOrder.flip₁_continuous'

deleted theorem Pi.OmegaCompletePartialOrder.flip₂_continuous'

added theorem ScottContinuous.ωScottContinuous

Created Mathlib/Order/ScottContinuity.lean

added theorem ScottContinuous.id

added theorem ScottContinuous.scottContinuousOn

added def ScottContinuous

added theorem ScottContinuousOn.id

added theorem ScottContinuousOn.mono

added theorem ScottContinuousOn.prodMk

added theorem ScottContinuousOn.sup₂

added def ScottContinuousOn

added theorem scottContinuousOn_univ

Modified Mathlib/Topology/OmegaCompletePartialOrder.lean

modified theorem Scott.IsOpen.isUpperSet

modified theorem Scott.isOpen_univ

Modified Mathlib/Topology/Order/ScottTopology.lean