Instances related to the discrete topology

We prove that the discrete topology is

• first-countable,
• second-countable for an encodable type,
• equal to the order topology in linear orders which are also PredOrder and SuccOrder,
• metrizable.

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

@[instance 100]

instance DiscreteTopology.firstCountableTopology {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] : FirstCountableTopology α

@[instance 100]

instance DiscreteTopology.secondCountableTopology_of_countable {α : Type u_1} [TopologicalSpace α] [hd : DiscreteTopology α] [Countable α] : SecondCountableTopology α

theorem LinearOrder.bot_topologicalSpace_eq_preorderTopology {α : Type u_2} [LinearOrder α] [PredOrder α] [SuccOrder α] : ⊥ = Preorder.topology α

@[deprecated LinearOrder.bot_topologicalSpace_eq_preorderTopology (since := "2026-03-22")]

theorem LinearOrder.bot_topologicalSpace_eq_generateFrom {α : Type u_2} [LinearOrder α] [PredOrder α] [SuccOrder α] : ⊥ = Preorder.topology α

Alias of LinearOrder.bot_topologicalSpace_eq_preorderTopology.

theorem discreteTopology_iff_orderTopology_of_pred_succ {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [PredOrder α] [SuccOrder α] : DiscreteTopology α ↔ OrderTopology α

instance OrderTopology.of_discreteTopology {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [PredOrder α] [SuccOrder α] [DiscreteTopology α] : OrderTopology α

instance OrderTopology.of_linearLocallyFinite {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [LocallyFiniteOrder α] [DiscreteTopology α] : OrderTopology α