Def Locale.PT

Modification history

2024-05-07 01:05

Mathlib/Topology/Order/Category/FrameAdjunction.lean

refactor: replace `@[reducible]` with `abbrev` (#12614) …

Deleted Locale.PT View on Github →

2023-10-21 09:35

Mathlib/Topology/Order/Category/FrameAdjunction.lean

feat: Adjunction between topological spaces and locales (#4593) …

Added Locale.PT View on Github →