α : Type u_1
β : Type u_2
γ : Type ?u.370133
δ : Type ?u.370136
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : OpenEmbedding f
s : Set β
x : α
⊢ 𝓝[s ∩ range f] f x = 𝓝[s] f x
α : Type u_1
β : Type u_2
γ : Type ?u.370133
δ : Type ?u.370136
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : OpenEmbedding f
s : Set β
x : α
⊢ map f (𝓝[f ⁻¹' s] x) = 𝓝[s] f x
rw [hf.toEmbedding.map_nhdsWithin_eq, image_preimage_eq_inter_range]
α : Type u_1
β : Type u_2
γ : Type ?u.370133
δ : Type ?u.370136
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : OpenEmbedding f
s : Set β
x : α
⊢ s ∩ range f ∩ range f = s ∩ range f
α : Type u_1
β : Type u_2
γ : Type ?u.370133
δ : Type ?u.370136
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : OpenEmbedding f
s : Set β
x : α
⊢ 𝓝[s ∩ range f] f x = 𝓝[s] f x
apply nhdsWithin_eq_nhdsWithin (mem_range_self _) hf.open_range
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.370133
δ : Type ?u.370136
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : OpenEmbedding f
s : Set β
x : α
⊢ s ∩ range f ∩ range f = s ∩ range f
rw [inter_assoc, inter_self]