uniqueDiffWithinAt_inter — Mathlib

English

If hs holds and t ∈ 𝓝 x, then UniqueDiffWithinAt 𝕜 (s ∩ t) x.

Русский

Если выполняется hs и t в окрестности x, то UniqueDiffWithinAt 𝕜 (s ∩ t) x.

LaTeX

$$$\\text{hs} \\; \\Rightarrow \\text{UniqueDiffWithinAt}_{\\mathbb{k}}(s \\cap t, x)$$$

Lean4

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

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