mathlib

e93996cf - feat(topology/instances/discrete): instances for the discrete topology (#11349)

feat(topology/instances/discrete): instances for the discrete topology (#11349) Prove `first_countable_topology`, `second_countable_topology` and `order_topology` for the discrete topology under appropriate conditions like `encodable`, or being a linear order with `pred` and `succ`. These instances give in particular `second_countable_topology ℕ` and `order_topology ℕ` Co-authored-by: RemyDegenne <remydegenne@gmail.com> Co-authored-by: Patrick Massot <patrickmassot@free.fr>