English
Let s and t be subsets of a normed space E and x ∈ E. If the neighborhood structures of s and t at x agree, then the tangent cones at x coincide: tangentConeAt(s, x) = tangentConeAt(t, x).
Русский
Пусть s и t — подмножества в нормированном пространстве E и x ∈ E. Если локальные окрестности x внутри s и внутри t совпадают, то касательные конусы в точке x совпадают: tangentConeAt(s, x) = tangentConeAt(t, x).
LaTeX
$$$\\operatorname{tangentCone}_{\\mathbb{k}}(s, x) = \\operatorname{tangentCone}_{\\mathbb{k}}(t, x) \\quad\\text{whenever } \\ nhds_{s}(x) = nhds_{t}(x)$$$
Lean4
/-- Tangent cone of `s` at `x` depends only on `𝓝[s] x`. -/
theorem tangentConeAt_congr (h : 𝓝[s] x = 𝓝[t] x) : tangentConeAt 𝕜 s x = tangentConeAt 𝕜 t x :=
Subset.antisymm (tangentConeAt_mono_nhds h.le) (tangentConeAt_mono_nhds h.ge)
