tangentConeAt_inter_nhds — Mathlib

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

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