[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ ∀ (a : α), IsCountablyGenerated (nhds a)
[PROOFSTEP]
rw [nhds_discrete]
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ ∀ (a : α), IsCountablyGenerated (pure a)
[PROOFSTEP]
exact isCountablyGenerated_pure
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
hd : DiscreteTopology α
inst✝ : Encodable α
i : α
⊢ instTopologicalSpaceSubtype = generateFrom {univ}
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
⊢ ⊥ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}
[PROOFSTEP]
refine' (eq_bot_of_singletons_open fun a => _).symm
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a : α
⊢ IsOpen {a}
[PROOFSTEP]
have h_singleton_eq_inter : { a } = Iio (succ a) ∩ Ioi (pred a) :=
  by
  suffices h_singleton_eq_inter' : { a } = Iic a ∩ Ici a
  · rw [h_singleton_eq_inter', ← Ioi_pred, ← Iio_succ]
  rw [inter_comm, Ici_inter_Iic, Icc_self a]
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a : α
⊢ {a} = Iio (succ a) ∩ Ioi (pred a)
[PROOFSTEP]
suffices h_singleton_eq_inter' : { a } = Iic a ∩ Ici a
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a : α
h_singleton_eq_inter' : {a} = Iic a ∩ Ici a
⊢ {a} = Iio (succ a) ∩ Ioi (pred a)
[PROOFSTEP]
rw [h_singleton_eq_inter', ← Ioi_pred, ← Iio_succ]
[GOAL]
case h_singleton_eq_inter'
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a : α
⊢ {a} = Iic a ∩ Ici a
[PROOFSTEP]
rw [inter_comm, Ici_inter_Iic, Icc_self a]
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
⊢ IsOpen {a}
[PROOFSTEP]
rw [h_singleton_eq_inter]
  -- Porting note: Specified instance for `IsOpen.inter` explicitly to fix an error.
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
⊢ IsOpen (Iio (succ a) ∩ Ioi (pred a))
[PROOFSTEP]
apply @IsOpen.inter _ _ _ (generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a})
[GOAL]
case h₁
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
⊢ IsOpen (Iio (succ a))
[PROOFSTEP]
exact isOpen_generateFrom_of_mem ⟨succ a, Or.inr rfl⟩
[GOAL]
case h₂
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
⊢ IsOpen (Ioi (pred a))
[PROOFSTEP]
exact isOpen_generateFrom_of_mem ⟨pred a, Or.inl rfl⟩
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
⊢ DiscreteTopology α ↔ OrderTopology α
[PROOFSTEP]
refine' ⟨fun h => ⟨_⟩, fun h => ⟨_⟩⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
h : DiscreteTopology α
⊢ inst✝⁵ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}
[PROOFSTEP]
rw [h.eq_bot]
[GOAL]
case refine'_1
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
h : DiscreteTopology α
⊢ ⊥ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}
[PROOFSTEP]
exact bot_topologicalSpace_eq_generateFrom_of_pred_succOrder
[GOAL]
case refine'_2
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
h : OrderTopology α
⊢ inst✝⁵ = ⊥
[PROOFSTEP]
rw [h.topology_eq_generate_intervals]
[GOAL]
case refine'_2
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : SuccOrder α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
h : OrderTopology α
⊢ generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} = ⊥
[PROOFSTEP]
exact bot_topologicalSpace_eq_generateFrom_of_pred_succOrder.symm
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
⊢ ⊥ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}
[PROOFSTEP]
refine' (eq_bot_of_singletons_open fun a => _).symm
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
⊢ IsOpen {a}
[PROOFSTEP]
have h_singleton_eq_inter : { a } = Iic a ∩ Ici a := by rw [inter_comm, Ici_inter_Iic, Icc_self a]
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
⊢ {a} = Iic a ∩ Ici a
[PROOFSTEP]
rw [inter_comm, Ici_inter_Iic, Icc_self a]
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iic a ∩ Ici a
⊢ IsOpen {a}
[PROOFSTEP]
by_cases ha_top : IsTop a
[GOAL]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iic a ∩ Ici a
ha_top : IsTop a
⊢ IsOpen {a}
[PROOFSTEP]
rw [ha_top.Iic_eq, inter_comm, inter_univ] at h_singleton_eq_inter 
[GOAL]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ici a
ha_top : IsTop a
⊢ IsOpen {a}
[PROOFSTEP]
by_cases ha_bot : IsBot a
[GOAL]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ici a
ha_top : IsTop a
ha_bot : IsBot a
⊢ IsOpen {a}
[PROOFSTEP]
rw [ha_bot.Ici_eq] at h_singleton_eq_inter 
[GOAL]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = univ
ha_top : IsTop a
ha_bot : IsBot a
⊢ IsOpen {a}
[PROOFSTEP]
rw [h_singleton_eq_inter]
  -- Porting note: Specified instance for `isOpen_univ` explicitly to fix an error.
[GOAL]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = univ
ha_top : IsTop a
ha_bot : IsBot a
⊢ IsOpen univ
[PROOFSTEP]
apply @isOpen_univ _ (generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a})
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ici a
ha_top : IsTop a
ha_bot : ¬IsBot a
⊢ IsOpen {a}
[PROOFSTEP]
rw [isBot_iff_isMin] at ha_bot 
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ici a
ha_top : IsTop a
ha_bot : ¬IsMin a
⊢ IsOpen {a}
[PROOFSTEP]
rw [← Ioi_pred_of_not_isMin ha_bot] at h_singleton_eq_inter 
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ioi (pred a)
ha_top : IsTop a
ha_bot : ¬IsMin a
⊢ IsOpen {a}
[PROOFSTEP]
rw [h_singleton_eq_inter]
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Ioi (pred a)
ha_top : IsTop a
ha_bot : ¬IsMin a
⊢ IsOpen (Ioi (pred a))
[PROOFSTEP]
exact isOpen_generateFrom_of_mem ⟨pred a, Or.inl rfl⟩
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iic a ∩ Ici a
ha_top : ¬IsTop a
⊢ IsOpen {a}
[PROOFSTEP]
rw [isTop_iff_isMax] at ha_top 
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iic a ∩ Ici a
ha_top : ¬IsMax a
⊢ IsOpen {a}
[PROOFSTEP]
rw [← Iio_succ_of_not_isMax ha_top] at h_singleton_eq_inter 
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ici a
ha_top : ¬IsMax a
⊢ IsOpen {a}
[PROOFSTEP]
by_cases ha_bot : IsBot a
[GOAL]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ici a
ha_top : ¬IsMax a
ha_bot : IsBot a
⊢ IsOpen {a}
[PROOFSTEP]
rw [ha_bot.Ici_eq, inter_univ] at h_singleton_eq_inter 
[GOAL]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a)
ha_top : ¬IsMax a
ha_bot : IsBot a
⊢ IsOpen {a}
[PROOFSTEP]
rw [h_singleton_eq_inter]
[GOAL]
case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a)
ha_top : ¬IsMax a
ha_bot : IsBot a
⊢ IsOpen (Iio (succ a))
[PROOFSTEP]
exact isOpen_generateFrom_of_mem ⟨succ a, Or.inr rfl⟩
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ici a
ha_top : ¬IsMax a
ha_bot : ¬IsBot a
⊢ IsOpen {a}
[PROOFSTEP]
rw [isBot_iff_isMin] at ha_bot 
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ici a
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen {a}
[PROOFSTEP]
rw [← Ioi_pred_of_not_isMin ha_bot] at h_singleton_eq_inter 
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen {a}
[PROOFSTEP]
rw [h_singleton_eq_inter]
  -- Porting note: Specified instance for `IsOpen.inter` explicitly to fix an error.
[GOAL]
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen (Iio (succ a) ∩ Ioi (pred a))
[PROOFSTEP]
apply @IsOpen.inter _ _ _ (generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a})
[GOAL]
case neg.h₁
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen (Iio (succ a))
[PROOFSTEP]
exact isOpen_generateFrom_of_mem ⟨succ a, Or.inr rfl⟩
[GOAL]
case neg.h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
a : α
h_singleton_eq_inter : {a} = Iio (succ a) ∩ Ioi (pred a)
ha_top : ¬IsMax a
ha_bot : ¬IsMin a
⊢ IsOpen (Ioi (pred a))
[PROOFSTEP]
exact isOpen_generateFrom_of_mem ⟨pred a, Or.inl rfl⟩
[GOAL]
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
⊢ DiscreteTopology α ↔ OrderTopology α
[PROOFSTEP]
refine' ⟨fun h => ⟨_⟩, fun h => ⟨_⟩⟩
[GOAL]
case refine'_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
h : DiscreteTopology α
⊢ inst✝³ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}
[PROOFSTEP]
rw [h.eq_bot]
[GOAL]
case refine'_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
h : DiscreteTopology α
⊢ ⊥ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}
[PROOFSTEP]
exact LinearOrder.bot_topologicalSpace_eq_generateFrom
[GOAL]
case refine'_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
h : OrderTopology α
⊢ inst✝³ = ⊥
[PROOFSTEP]
rw [h.topology_eq_generate_intervals]
[GOAL]
case refine'_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
h : OrderTopology α
⊢ generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} = ⊥
[PROOFSTEP]
exact LinearOrder.bot_topologicalSpace_eq_generateFrom.symm
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ MetrizableSpace α
[PROOFSTEP]
obtain rfl := DiscreteTopology.eq_bot (α := α)
[GOAL]
α : Type u_1
inst✝ : DiscreteTopology α
⊢ MetrizableSpace α
[PROOFSTEP]
exact @UniformSpace.metrizableSpace α ⊥ (isCountablyGenerated_principal _) _
