Commit 2022-02-14 21:58 efdce094View on Github →
cofinite_topology into a type synonym (#11967)
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
over the place.
topology.alexandroff and prove it for
alexandroff ℕ and
cofinite_topology (alexandroff ℕ).