English
If x is not an accumulation point of s, then tangentConeAt(s, x) ⊆ {0}.
Русский
Если x не является точкой накопления множества s, то tangentConeAt(s,x) ⊆ {0}.
LaTeX
$$$\\operatorname{tangentCone}_{\\mathbb{k}}(s, x) \\subseteq \\{0\\}$$$
Lean4
/-- If `x` is not an accumulation point of `s, then the tangent cone of `s` at `x`
is a subset of `{0}`. -/
theorem tangentConeAt_subset_zero (hx : ¬AccPt x (𝓟 s)) : tangentConeAt 𝕜 s x ⊆ 0 :=
by
rintro y ⟨c, d, hds, hc, hcd⟩
suffices ∀ᶠ n in .atTop, d n = 0 from
tendsto_nhds_unique hcd <| tendsto_const_nhds.congr' <| this.mono fun n hn ↦ by simp [hn]
simp only [accPt_iff_frequently, not_frequently, not_and', ne_eq, not_not] at hx
have : Tendsto (x + d ·) atTop (𝓝 x) := by simpa using tendsto_const_nhds.add (tangentConeAt.lim_zero _ hc hcd)
filter_upwards [this.eventually hx, hds] with n h₁ h₂
simpa using h₁ h₂
