Tangent cone in a proper space

In this file we prove that the tangent cone of a set in a proper normed space at an accumulation point of this set is nontrivial.

theorem tangentConeAt_nonempty_of_properSpace {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [ProperSpace E] {s : Set E} {x : E} (hx : AccPt x (Filter.principal s)) : (tangentConeAt 𝕜 s x ∩ {0}ᶜ).Nonempty

In a proper space, the tangent cone at a non-isolated point is nontrivial.