uniqueDiffWithinAt_of_mem_nhds — Mathlib

English

Let 𝕜 be a nontrivially normed field and E a normed 𝕜-space. If s ⊆ E and x ∈ E with s ∈ 𝓝(x) (i.e., s contains a neighborhood of x), then s is uniquely differentiable at x with respect to 𝕜.

Русский

Пусть 𝕜 — ненулевое нормированное поле, E — нормированное пространство над 𝕜. Если s ⊆ E и x ∈ E и s содержится в окрестности x, то в точке x множество s обладает уникальной дифференцируемостью относительно 𝕜.

LaTeX

$$$ s \in \\mathcal{N}(x) \\Rightarrow \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}}(s,x) $$$

Lean4

theorem uniqueDiffWithinAt_of_mem_nhds (h : s ∈ 𝓝 x) : UniqueDiffWithinAt 𝕜 s x := by
  simpa only [univ_inter] using uniqueDiffWithinAt_univ.inter h

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