Documentation

Mathlib.Topology.Instances.Discrete

Instances related to the discrete topology #

We prove that the discrete topology is

When importing this file and Data.Nat.SuccPred, the instances SecondCountableTopology ℕ and OrderTopology become available.