I realised that I’ve never ported the definition of a sublocale from `ayberkt/formal-topology-in-UF`. It’s probably a good idea to do this.
I realised that I’ve never ported the definition of a sublocale from
ayberkt/formal-topology-in-UF. It’s probably a good idea to do this.