α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ (s : Set β), s ∈ B → IsOpen (f ⁻¹' s)
⊢ Continuous f
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ (s : Set β), s ∈ B → IsOpen (f ⁻¹' s)
⊢ Continuous f
rw [hB.eq_generateFrom]
no goals
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ (s : Set β), s ∈ B → IsOpen (f ⁻¹' s)
⊢ Continuous f
exact continuous_generateFrom hf