mathlib documentation

topology.instances.discrete

Instances related to the discrete topology #

We prove that the discrete topology is

When importing this file and data.nat.succ_pred, the instances second_countable_topology ℕ and order_topology become available.