uniqueDiffWithinAt — Mathlib

English

If a set has UniqueDiffOn 𝕜 s, then every x ∈ s has UniqueDiffWithinAt 𝕜 s x.

Русский

Если множество обладает свойством UniqueDiffOn 𝕜 s, то для любой точки x ∈ s верно UniqueDiffWithinAt 𝕜 s x.

LaTeX

$$$\\text{UniqueDiffOn}_{\\mathbb{k}}(s) \\Rightarrow \\forall x \\in s,\\; \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}}(s, x)$$$

Lean4

theorem uniqueDiffWithinAt {s : Set E} {x} (hs : UniqueDiffOn 𝕜 s) (h : x ∈ s) : UniqueDiffWithinAt 𝕜 s x :=
  hs x h

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