case intro
α : Type u_2
β : Type u_1
γ : Type ?u.8061
δ : Type ?u.8064
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : { x // x ∈ t }
hs : s ∈ 𝓝 (π ↑a)
⊢ π ⁻¹' s ∈ 𝓝[t] ↑a
α : Type u_2
β : Type u_1
γ : Type ?u.8061
δ : Type ?u.8064
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
hs : s ∈ 𝓝 (π a)
⊢ π ⁻¹' s ∈ 𝓝[t] a
lift a to t using h
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.8061
δ : Type ?u.8064
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : { x // x ∈ t }
hs : (fun x => π ↑x) ⁻¹' s ∈ 𝓝 a
⊢ π ⁻¹' s ∈ 𝓝[t] ↑a
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.8061
δ : Type ?u.8064
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : { x // x ∈ t }
hs : s ∈ 𝓝 (π ↑a)
⊢ π ⁻¹' s ∈ 𝓝[t] ↑a
replace hs : (fun x : t => π x) ⁻¹' s ∈ 𝓝 a := preimage_nhds_coinduced hs
no goals
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.8061
δ : Type ?u.8064
inst✝ : TopologicalSpace α
π : α → β
s : Set β
t : Set α
a : { x // x ∈ t }
hs : (fun x => π ↑x) ⁻¹' s ∈ 𝓝 a
⊢ π ⁻¹' s ∈ 𝓝[t] ↑a
rwa [← map_nhds_subtype_val, mem_map]