Unique differentiability property of a set in the base field #
In this file we prove that a set in the base field has the unique differentiability property at x
iff x is an accumulation point of the set, see uniqueDiffWithinAt_iff_accPt.
theorem
tangentConeAt_eq_univ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{s : Set 𝕜}
{x : 𝕜}
(hx : AccPt x (Filter.principal s))
:
The tangent cone at a non-isolated point in dimension 1 is the whole space.
@[deprecated tangentConeAt_eq_univ (since := "2025-04-27")]
theorem
tangentCone_eq_univ
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{s : Set 𝕜}
{x : 𝕜}
(hx : AccPt x (Filter.principal s))
:
Alias of tangentConeAt_eq_univ.
The tangent cone at a non-isolated point in dimension 1 is the whole space.
theorem
uniqueDiffWithinAt_iff_accPt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{s : Set 𝕜}
{x : 𝕜}
:
In one dimension, a point is a point of unique differentiability of a set iff it is an accumulation point of the set.
theorem
AccPt.uniqueDiffWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{s : Set 𝕜}
{x : 𝕜}
:
AccPt x (Filter.principal s) → UniqueDiffWithinAt 𝕜 s x
Alias of the reverse direction of uniqueDiffWithinAt_iff_accPt.
In one dimension, a point is a point of unique differentiability of a set iff it is an accumulation point of the set.