case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : SeparableSpace α
s : Set α
hc : Set.Countable s
hd : Dense s
⊢ SecondCountableTopology α
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : SeparableSpace α
⊢ SecondCountableTopology α
rcases exists_countable_dense α with ⟨s, hc, hd⟩
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : SeparableSpace α
s : Set α
hc : Set.Countable s
hd : Dense s
⊢ Set.Countable (Ioi '' s ∪ Iio '' s)
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : SeparableSpace α
s : Set α
hc : Set.Countable s
hd : Dense s
⊢ SecondCountableTopology α
refine ⟨⟨_, ?_, hd.topology_eq_generateFrom⟩⟩
no goals
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : SeparableSpace α
s : Set α
hc : Set.Countable s
hd : Dense s
⊢ Set.Countable (Ioi '' s ∪ Iio '' s)
exact (hc.image _).union (hc.image _)