α : Type u_1
β : Type u_2
γ : Type ?u.3026
δ : Type ?u.3029
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
a : α
l : Filter α
⊢ NeBot (𝓝 (f a) ⊓ map f l) ↔ NeBot (𝓝 a ⊓ l)
α : Type u_1
β : Type u_2
γ : Type ?u.3026
δ : Type ?u.3029
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
a : α
l : Filter α
⊢ MapClusterPt (f a) l f ↔ ClusterPt a l
delta MapClusterPt ClusterPt
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.3026
δ : Type ?u.3029
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
a : α
l : Filter α
⊢ NeBot (𝓝 (f a) ⊓ map f l) ↔ NeBot (𝓝 a ⊓ l)
rw [← Filter.push_pull', ← hf.nhds_eq_comap, map_neBot_iff]