Commit 2023-09-05 23:13 44f55245
View on Github →feat: Alexandrov-discrete spaces (#6962)
We define Alexandrov-discrete spaces as topological spaces where the intersection of a family of open sets is open.
This PR only gives a minimal API because the goal is to ensure that lemma names like isOpen_sInter are free to use for AlexandrovDiscrete. The existing lemmas are getting prefixed by Set.Finite or suffixed by _of_finite.