English
Intersecting s with a neighborhood of x does not change the tangent cone: tangentConeAt(𝕜, s ∩ t, x) = tangentConeAt(𝕜, s, x) when t ∈ 𝓝 x.
Русский
Пересечение s с окрестностью x не изменяет касательный конус: tangentConeAt(𝕜, s ∩ t, x) = tangentConeAt(𝕜, s, x), если t ∈ 𝓝 x.
LaTeX
$$$\\operatorname{tangentCone}_{\\mathbb{k}}(s \\cap t, x) = \\operatorname{tangentCone}_{\\mathbb{k}}(s, x) \\quad\\text{provided } t \\in \\mathcal{N}(x)$$$
Lean4
/-- Intersecting with a neighborhood of the point does not change the tangent cone. -/
theorem tangentConeAt_inter_nhds (ht : t ∈ 𝓝 x) : tangentConeAt 𝕜 (s ∩ t) x = tangentConeAt 𝕜 s x :=
tangentConeAt_congr (nhdsWithin_restrict' _ ht).symm