Theorem Locale.PT.isOpen_iff

Modification history

2023-10-21 09:35
Mathlib/Topology/Order/Category/FrameAdjunction.lean
feat: Adjunction between topological spaces and locales (#4593) …
Added Locale.PT.isOpen_iffView on Github →