English
If E is a normed space over 𝕜 ⊆ 𝕜' and x ∈ s is a point with UniqueDiffWithinAt 𝕜 s x, then x is a point with UniqueDiffWithinAt 𝕜' s x.
Русский
Пусть E является нормированным пространством над полем 𝕜, вложенном в 𝕜'. Если x ∈ s и в точке x существуют уникальные дифференцируемости относительно 𝕜, то эти свойства сохраняются и относительно 𝕜'.
LaTeX
$$$ \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}}(s,x) \\Rightarrow \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}'}(s,x) $$$
Lean4
/-- Given `x ∈ s` and a field extension `𝕜 ⊆ 𝕜'`, the tangent cone of `s` at `x` with
respect to `𝕜` is contained in the tangent cone of `s` at `x` with respect to `𝕜'`.
-/
theorem tangentConeAt_mono_field : tangentConeAt 𝕜 s x ⊆ tangentConeAt 𝕜' s x :=
by
intro α hα
simp only [tangentConeAt, eventually_atTop, ge_iff_le, tendsto_norm_atTop_iff_cobounded, mem_setOf_eq] at hα ⊢
obtain ⟨c, d, ⟨a, h₁a⟩, h₁, h₂⟩ := hα
use ((algebraMap 𝕜 𝕜') ∘ c), d
constructor
· use a
· constructor
· intro β hβ
rw [mem_map, mem_atTop_sets]
obtain ⟨n, hn⟩ := mem_atTop_sets.1 (mem_map.1 (h₁ (algebraMap_cobounded_le_cobounded (𝕜 := 𝕜) (𝕜' := 𝕜') hβ)))
use n, fun _ _ ↦ by simp_all
· simpa
