Commit 2024-02-09 19:11 c721d5cc

View on Github →

refactor(Topology/Order) : Fix inconsistencies between Lower/Upper and Scott topologies (#10346)

Make type explicit in def of Scott-Hausdorff and Scott topologies
Move With{Lower|Upper}Homeomorph into the correct namespace

Estimated changes

Modified Mathlib/Topology/Order/LowerUpperTopology.lean

deleted def Topology.IsLower.WithLowerHomeomorph

added def Topology.IsLower.withLowerHomeomorph

deleted def Topology.IsUpper.WithUpperHomeomorph

added def Topology.IsUpper.withUpperHomeomorph

Modified Mathlib/Topology/Order/ScottTopology.lean

modified theorem Topology.IsLower.scottHausdorff_le

modified theorem Topology.IsScott.scottHausdorff_le

modified theorem Topology.IsScott.topology_eq

added def Topology.IsScott.withScottHomeomorph

modified theorem Topology.IsScottHausdorff.topology_eq

deleted def Topology.WithScott.withScottHomeomorph

modified def Topology.scott

modified def Topology.scottHausdorff

modified theorem Topology.upperSet_le_scott