mathlib3 documentation

topology.instances.discrete

Instances related to the discrete topology #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.