English
In one dimension, every point is either a point of unique differentiability for s, or the nhdsWithin of x in s\{x} is the bottom filter (i.e., x is isolated from s).
Русский
В одном измерении каждая точка либо является точкой уникальной дифференцируемости множества s, либо nhdsWithin(x; s \ {x}) = ⊥, то есть x изолирован от s.
LaTeX
$$$\mathrm{UniqueDiffWithinAt}\,\mathbb{R}\,s\,x \lor \mathcal{N}hds_{s\setminus\{x\}}(x) = \bot$$$
Lean4
/-- In one dimension, every point is either a point of unique differentiability, or isolated. -/
@[deprecated uniqueDiffWithinAt_iff_accPt (since := "2025-04-20")]
theorem uniqueDiffWithinAt_or_nhdsWithin_eq_bot (s : Set 𝕜) (x : 𝕜) : UniqueDiffWithinAt 𝕜 s x ∨ 𝓝[s \ { x }] x = ⊥ :=
(em (AccPt x (𝓟 s))).imp AccPt.uniqueDiffWithinAt fun h ↦ by rwa [accPt_principal_iff_nhdsWithin, not_neBot] at h
