English
If h is a UniqueDiffWithinAt on s and s ⊆ closure(t), then UniqueDiffWithinAt on t.
Русский
Если для множества s выполнено уникальное дифференцируемость, и s ⊆ closure(t), то уникальная дифференцируемость переносится на t.
LaTeX
$$$ \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}}(s,x) \\land (s \\subseteq \\overline{t}) \\Rightarrow \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}}(t,x) $$$
Lean4
/-- Assume that `E` is a normed vector space over normed fields `𝕜 ⊆ 𝕜'` and all points of `s` are
points of unique differentiability with respect to the smaller field `𝕜`, then they are also points
of unique differentiability with respect to the larger field `𝕜`.
-/
theorem mono_field (h₂s : UniqueDiffOn 𝕜 s) : UniqueDiffOn 𝕜' s := fun x hx ↦ (h₂s x hx).mono_field
