English
If h₂s holds for 𝕜, then it holds for 𝕜' across s, i.e., pointwise Monotone field extension preserves unique differentiability.
Русский
Если множество s имеет уникальную дифференцируемость относительно 𝕜, то она сохраняется при переходе к 𝕜'.
LaTeX
$$$ \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}}(s) \\Rightarrow \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}'}(s) $$$
Lean4
/-- Assume that `E` is a normed vector space over normed fields `𝕜 ⊆ 𝕜'` and that `x ∈ s` is a point
of unique differentiability with respect to the set `s` and the smaller field `𝕜`, then `x` is also
a point of unique differentiability with respect to the set `s` and the larger field `𝕜'`.
-/
theorem mono_field (h₂s : UniqueDiffWithinAt 𝕜 s x) : UniqueDiffWithinAt 𝕜' s x :=
by
simp_all only [uniqueDiffWithinAt_iff, and_true]
apply Dense.mono _ h₂s.1
trans ↑(Submodule.span 𝕜 (tangentConeAt 𝕜' s x)) <;> simp [Submodule.span_mono tangentConeAt_mono_field]
