Def WithLowerSetTopology

Modification history

2023-09-24 19:47

Mathlib/Topology/Order/UpperLowerSetTopology.lean

refactor(Topology/Order): Rename order topologies (#7310) …

Deleted WithLowerSetTopology View on Github →

2023-09-08 07:26

Mathlib/Topology/Order/UpperLowerSetTopology.lean

feat: Functoriality of `WithUpperSetTopology` (#6988) …

Modified WithLowerSetTopology View on Github →

2023-08-01 18:11

Mathlib/Topology/Order/UpperLowerSetTopology.lean

feat(Topology/Order/UpperLowerSetTopology): Introduce the Upper Set (or Alexandrov) topology and the Lower Set topology (#5672) …

Added WithLowerSetTopology View on Github →