uniqueDiffWithinAt_iff_accPt — Mathlib

English

In one dimension, a point x is a point of unique differentiability for a set s if and only if x is an accumulation point of s.

Русский

В одном измерении точка x является точкой уникальной дифференцируемости множества s если и только если x является точкой накопления множества s.

LaTeX

$$$\mathrm{UniqueDiffWithinAt}_{\mathbb{R}}(s,x) \ \Longleftrightarrow\ \mathrm{AccPt}\,x\,(\mathcal{P}s)$$$

Lean4

/-- In one dimension, a point is a point of unique differentiability of a set
iff it is an accumulation point of the set. -/
theorem uniqueDiffWithinAt_iff_accPt {s : Set 𝕜} {x : 𝕜} : UniqueDiffWithinAt 𝕜 s x ↔ AccPt x (𝓟 s) :=
  ⟨UniqueDiffWithinAt.accPt, fun h ↦ ⟨by simp [tangentConeAt_eq_univ h], mem_closure_iff_clusterPt.mpr h.clusterPt⟩⟩

Похожие утверждения