Commit 2022-02-14 21:58 efdce094

refactor(topology/constructions): turn cofinite_topology into a type synonym (#11967) Instead of cofinite_topology α : topological_space α, define cofinite_topology α := α with an instance topological_space (cofinite_topology α) := (old definition). This way we can talk about cofinite topology without using @ all over the place. Also move homeo_of_equiv_compact_to_t2.t1_counterexample to topology.alexandroff and prove it for alexandroff ℕ and cofinite_topology (alexandroff ℕ).