uniqueDiffWithinAt — Mathlib

English

If s is open and x ∈ s, then s has unique differentiability at x with respect to 𝕜.

Русский

Пусть s — открытое множество, и x ∈ s. Тогда в точке x множество s имеет уникальную дифференцируемость относительно 𝕜.

LaTeX

$$$ \\text{IsOpen}(s) \\land x \\in s \\Rightarrow \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}}(s,x) $$$

Lean4

theorem uniqueDiffWithinAt (hs : IsOpen s) (xs : x ∈ s) : UniqueDiffWithinAt 𝕜 s x :=
  uniqueDiffWithinAt_of_mem_nhds (IsOpen.mem_nhds hs xs)

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