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

• (_ : FirstCountableTopology α) = (_ : FirstCountableTopology α)

instance DiscreteTopology.secondCountableTopology_of_encodable {α : Type u_1} [TopologicalSpace α] [hd : DiscreteTopology α] [Encodable α] : SecondCountableTopology α

Equations

• (_ : SecondCountableTopology α) = (_ : 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

• (_ : OrderTopology α) = (_ : OrderTopology α)

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

• (_ : OrderTopology α) = (_ : OrderTopology α)

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

Equations

• (_ : TopologicalSpace.MetrizableSpace α) = (_ : TopologicalSpace.MetrizableSpace α)