case intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : Set.Countable b
eq : t = generateFrom b
⊢ SecondCountableTopology α
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
⊢ SecondCountableTopology α
rcases @SecondCountableTopology.is_open_generated_countable β _ _ with ⟨b, hb, eq⟩
case intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : Set.Countable b
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ SecondCountableTopology α
case intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : Set.Countable b
eq : t = generateFrom b
⊢ SecondCountableTopology α
letI := t.induced f
case intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : Set.Countable b
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ induced f t = generateFrom (preimage f '' b)
case intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : Set.Countable b
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ SecondCountableTopology α
refine' { is_open_generated_countable := ⟨preimage f '' b, hb.image _, _⟩ }
no goals
case intro.intro
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : Set.Countable b
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ induced f t = generateFrom (preimage f '' b)
rw [eq, induced_generateFrom_eq]