Commit 2025-07-02 15:47 ff1ed482

View on Github →

chore: deprecate Scott in favour of WithScott (#26619) This type synonym is a duplicate and badly implemented (it is an abbrev). Also fix a few misnamed lemmas about the Scott topology. Closes #26494.

Estimated changes

Modified Mathlib/Topology/OmegaCompletePartialOrder.lean

added theorem Topology.IsScott.ωScottContinuous_iff_continuous

deleted theorem Topology.IsScott.ωscottContinuous_iff_continuous

modified def notBelow

modified theorem notBelow_isOpen

Modified Mathlib/Topology/Order/LawsonTopology.lean

deleted theorem Topology.IsLawson.singleton_isClosed

Modified Mathlib/Topology/Order/ScottTopology.lean

deleted theorem Topology.IsScott.isClosed_Iic

added theorem Topology.IsScott.scottContinuousOn_iff_continuous

deleted theorem Topology.IsScott.scottContinuous_iff_continuous