α : Type u_1
β : Type u_2
γ : Type ?u.20836
inst✝ : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
this : TopologicalSpace β := TopologicalSpace.coinduced π inst✝
⊢ π ⁻¹' s ∈ 𝓝 a
α : Type u_1
β : Type u_2
γ : Type ?u.20836
inst✝ : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
⊢ π ⁻¹' s ∈ 𝓝 a
letI := TopologicalSpace.coinduced π ‹_›
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.20836
inst✝ : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
this : TopologicalSpace β := TopologicalSpace.coinduced π inst✝
V : Set β
hVs : V ⊆ s
V_op : IsOpen V
mem_V : π a ∈ V
⊢ π ⁻¹' s ∈ 𝓝 a
α : Type u_1
β : Type u_2
γ : Type ?u.20836
inst✝ : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
this : TopologicalSpace β := TopologicalSpace.coinduced π inst✝
⊢ π ⁻¹' s ∈ 𝓝 a
rcases mem_nhds_iff.mp hs with ⟨V, hVs, V_op, mem_V⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.20836
inst✝ : TopologicalSpace α
π : α → β
s : Set β
a : α
hs : s ∈ 𝓝 (π a)
this : TopologicalSpace β := TopologicalSpace.coinduced π inst✝
V : Set β
hVs : V ⊆ s
V_op : IsOpen V
mem_V : π a ∈ V
⊢ π ⁻¹' s ∈ 𝓝 a
exact mem_nhds_iff.mpr ⟨π ⁻¹' V, Set.preimage_mono hVs, V_op, mem_V⟩