no goals
α : Type u
β : Type v
γ : Type ?u.11692
δ : Type ?u.11695
ε : Type ?u.11698
ζ : Type ?u.11701
inst✝ : TopologicalSpace α
s t : Set α
x : ↑s
⊢ 𝓝[Subtype.val ⁻¹' t] x = ⊥ ↔ 𝓝[t] ↑x ⊓ 𝓟 s = ⊥
rw [inf_principal_eq_bot_iff_comap, nhdsWithin, nhdsWithin, comap_inf, comap_principal,
  nhds_induced]