Theorem TopologicalSpace.Opens.mk_empty

Modification history

2023-10-21 09:35
Mathlib/Topology/Sets/Opens.lean
feat: Adjunction between topological spaces and locales (#4593) …
Added TopologicalSpace.Opens.mk_emptyView on Github →