congr_pt — Mathlib

English

If h : UniqueDiffWithinAt 𝕜 s x and hy : x = y, then UniqueDiffWithinAt 𝕜 s y.

Русский

Если есть уникальная дифференцируемость внутри s в x и x = y, то сохраняется для y.

LaTeX

$$$\\text{UniqueDiffWithinAt}_{\\mathbb{k}}(s,x) \\Rightarrow \\text{UniqueDiffWithinAt}_{\\mathbb{k}}(s,y) \\quad (y=x)$$$

Lean4

theorem congr_pt (h : UniqueDiffWithinAt 𝕜 s x) (hy : x = y) : UniqueDiffWithinAt 𝕜 s y :=
  hy ▸ h

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