case intro.intro.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
π : X → Y
inst✝ : SecondCountableTopology X
h' : QuotientMap π
h : IsOpenMap π
V : Set (Set X)
V_countable : Set.Countable V
V_generates : IsTopologicalBasis V
⊢ ∃ b, Set.Countable b ∧ inst✝¹ = generateFrom b
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
π : X → Y
inst✝ : SecondCountableTopology X
h' : QuotientMap π
h : IsOpenMap π
⊢ ∃ b, Set.Countable b ∧ inst✝¹ = generateFrom b
obtain ⟨V, V_countable, -, V_generates⟩ := exists_countable_basis X
no goals
case intro.intro.intro
α : Type u
t : TopologicalSpace α
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
π : X → Y
inst✝ : SecondCountableTopology X
h' : QuotientMap π
h : IsOpenMap π
V : Set (Set X)
V_countable : Set.Countable V
V_generates : IsTopologicalBasis V
⊢ ∃ b, Set.Countable b ∧ inst✝¹ = generateFrom b
exact ⟨Set.image π '' V, V_countable.image (Set.image π),
  (V_generates.quotientMap h' h).eq_generateFrom⟩