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} [NormedDivisionRing 𝕜] {s : Set 𝕜} {x : 𝕜} (hx : AccPt x (Filter.principal s)) : tangentConeAt 𝕜 s x = Set.univ

The tangent cone at a non-isolated point in dimension 1 is the whole space.

theorem uniqueDiffWithinAt_iff_accPt {𝕜 : Type u_1} [NormedDivisionRing 𝕜] {s : Set 𝕜} {x : 𝕜} : UniqueDiffWithinAt 𝕜 s x ↔ AccPt x (Filter.principal s)

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} [NormedDivisionRing 𝕜] {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.