Def Locale.openOfElementHom

Modification history

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