case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : Set.Countable b
hb₂ : t = generateFrom b
⊢ ∃ b, Set.Countable b ∧ ¬∅ ∈ b ∧ IsTopologicalBasis b
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
⊢ ∃ b, Set.Countable b ∧ ¬∅ ∈ b ∧ IsTopologicalBasis b
obtain ⟨b, hb₁, hb₂⟩ := @SecondCountableTopology.is_open_generated_countable α _ _
case intro.intro.refine'_1
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : Set.Countable b
hb₂ : t = generateFrom b
⊢ Set.Countable ((fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ b} \ {∅})

case intro.intro.refine'_2
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : Set.Countable b
hb₂ : t = generateFrom b
⊢ ∅ ∈ {∅}
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : Set.Countable b
hb₂ : t = generateFrom b
⊢ ∃ b, Set.Countable b ∧ ¬∅ ∈ b ∧ IsTopologicalBasis b
refine' ⟨_, _, not_mem_diff_of_mem _, (isTopologicalBasis_of_subbasis hb₂).diff_empty⟩
no goals
case intro.intro.refine'_1
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : Set.Countable b
hb₂ : t = generateFrom b
⊢ Set.Countable ((fun f => ⋂₀ f) '' {f | Set.Finite f ∧ f ⊆ b} \ {∅})

case intro.intro.refine'_2
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
b : Set (Set α)
hb₁ : Set.Countable b
hb₂ : t = generateFrom b
⊢ ∅ ∈ {∅}
exacts [((countable_setOf_finite_subset hb₁).image _).mono (diff_subset _ _), rfl]