uniqueDiffWithinAt_inter' — Mathlib

English

If ht is in nhdsWithin x s, then tangent cone at s ∩ t equals tangent cone at s.

Русский

Если ht ∈ nhdsWithin x s, то tangentCone s∩t x = tangentCone s x.

LaTeX

$$$ht \\in nhdsWithin(x,s) \\Rightarrow UniqueDiffWithinAt( s \\cap t, x) \\Leftrightarrow UniqueDiffWithinAt(s, x)$$$

Lean4

theorem uniqueDiffWithinAt_inter' (ht : t ∈ 𝓝[s] x) : UniqueDiffWithinAt 𝕜 (s ∩ t) x ↔ UniqueDiffWithinAt 𝕜 s x :=
  uniqueDiffWithinAt_congr <| (nhdsWithin_restrict'' _ ht).symm

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