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))
:
In a proper space, the tangent cone at a non-isolated point is nontrivial.
@[deprecated tangentConeAt_nonempty_of_properSpace (since := "2025-04-27")]
theorem
tangentCone_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))
:
Alias of tangentConeAt_nonempty_of_properSpace.
In a proper space, the tangent cone at a non-isolated point is nontrivial.