English
A set s has UniqueDiffOn 𝕜 if at every point x∈s, x has a unique differentiable structure in s.
Русский
Множество s имеет свойство уникальности дифференциаций: в каждой точке x∈s существует единственная допустимая точка дифференцирования в ограниченной области.
LaTeX
$$$\text{UniqueDiffOn}(s) := ∀ x∈s,\ UniqueDiffWithinAt 𝕜 s x.$$$
Lean4
/-- A property ensuring that the tangent cone to `s` at any of its points spans a dense subset of
the whole space. The main role of this property is to ensure that the differential along `s` is
unique, hence this name. The uniqueness it asserts is proved in `UniqueDiffOn.eq` in
`Mathlib/Analysis/Calculus/FDeriv/Basic.lean`. -/
def UniqueDiffOn (s : Set E) : Prop :=
∀ x ∈ s, UniqueDiffWithinAt 𝕜 s x
