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 DiscreteTopology.firstCountableTopology {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] : FirstCountableTopology α

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[deprecated DiscreteTopology.secondCountableTopology_of_countable]

theorem DiscreteTopology.secondCountableTopology_of_encodable {α : Type u_2} [TopologicalSpace α] [DiscreteTopology α] [Countable α] : SecondCountableTopology α

theorem bot_topologicalSpace_eq_generateFrom_of_pred_succOrder {α : Type u_1} [PartialOrder α] [PredOrder α] [SuccOrder α] [NoMinOrder α] [NoMaxOrder α] : ⊥ = TopologicalSpace.generateFrom {s : Set α | ∃ (a : α), s = Set.Ioi a ∨ s = Set.Iio a}

theorem discreteTopology_iff_orderTopology_of_pred_succ' {α : Type u_1} [TopologicalSpace α] [PartialOrder α] [PredOrder α] [SuccOrder α] [NoMinOrder α] [NoMaxOrder α] : DiscreteTopology α ↔ OrderTopology α

instance DiscreteTopology.orderTopology_of_pred_succ' {α : Type u_1} [TopologicalSpace α] [h : DiscreteTopology α] [PartialOrder α] [PredOrder α] [SuccOrder α] [NoMinOrder α] [NoMaxOrder α] : OrderTopology α

Equations

• ⋯ = ⋯

theorem LinearOrder.bot_topologicalSpace_eq_generateFrom {α : Type u_1} [LinearOrder α] [PredOrder α] [SuccOrder α] : ⊥ = TopologicalSpace.generateFrom {s : Set α | ∃ (a : α), s = Set.Ioi a ∨ s = Set.Iio a}

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

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

Equations

• ⋯ = ⋯

instance DiscreteTopology.metrizableSpace {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] : TopologicalSpace.MetrizableSpace α

Equations

• ⋯ = ⋯