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.

@[instance 100]
Equations
  • =
@[deprecated DiscreteTopology.secondCountableTopology_of_countable]
@[instance 100]
Equations
  • =
@[instance 100]
Equations
  • =