Commit 2023-10-09 21:43 0bf6843f

feat(Topology/Separation): filter of codiscrete sets (#7456) This PR shows that, in any topological space, the sets whose complement is discrete and closed form a filter. (The only somewhat nontrivial step is to check that unions of discrete closed sets are discrete.) This is intended as a preliminary for introducing meromorphic functions on opens in $\mathbb{C}$ (which are, by definition, holomorphic on a co-discrete set).