accPt — Mathlib

English

In a proper space, if x is accumulation point of s, then the tangent cone at x is nontrivial: tangentConeAt(s, x) ∩ {0}^c ≠ ∅.

Русский

В корректном пространстве при точке x, являющейся точкой накопления множества s, касательный конус в x непуст: tangentConeAt(s,x) ∩ {0}^c ≠ ∅.

LaTeX

$$$(\\operatorname{tangentCone}_{\\mathbb{k}}(s, x) \\cap \\{0\\}^{\\complement}) \\neq \\emptyset$$$

Lean4

theorem accPt [Nontrivial E] (h : UniqueDiffWithinAt 𝕜 s x) : AccPt x (𝓟 s) :=
  by
  by_contra! h'
  have : Dense (Submodule.span 𝕜 (0 : Set E) : Set E) := h.1.mono <| by gcongr; exact tangentConeAt_subset_zero h'
  simp [dense_iff_closure_eq] at this

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