α : Type u_2
β : Type ?u.166489
γ : Type ?u.166492
δ : Type ?u.166495
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
M₀ : Type u_1
inst✝ : Zero M₀
a : α
f : α → M₀
⊢ f =ᶠ[𝓝 a] 0 ↔ {x | f x = 0} ∈ 𝓝 a
α : Type u_2
β : Type ?u.166489
γ : Type ?u.166492
δ : Type ?u.166495
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
M₀ : Type u_1
inst✝ : Zero M₀
a : α
f : α → M₀
⊢ f =ᶠ[𝓝 a] 0 ↔ ¬a ∈ closure (Function.support f)
rw [← mem_compl_iff, ← interior_compl, mem_interior_iff_mem_nhds, Function.compl_support]
no goals
α : Type u_2
β : Type ?u.166489
γ : Type ?u.166492
δ : Type ?u.166495
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
M₀ : Type u_1
inst✝ : Zero M₀
a : α
f : α → M₀
⊢ f =ᶠ[𝓝 a] 0 ↔ {x | f x = 0} ∈ 𝓝 a
rfl