Relationships between unique differentiability over ℝ and ℂ

A set of unique differentiability for ℝ is also a set of unique differentiability for ℂ (or for a general field satisfying IsRCLikeNormedField 𝕜).

theorem tangentConeAt_real_subset_isRCLikeNormedField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [h𝕜 : IsRCLikeNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] {s : Set E} {x : E} : tangentConeAt ℝ s x ⊆ tangentConeAt 𝕜 s x

theorem UniqueDiffWithinAt.of_real {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [h𝕜 : IsRCLikeNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] {s : Set E} {x : E} (hs : UniqueDiffWithinAt ℝ s x) : UniqueDiffWithinAt 𝕜 s x

theorem UniqueDiffOn.of_real {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [h𝕜 : IsRCLikeNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] {s : Set E} (hs : UniqueDiffOn ℝ s) : UniqueDiffOn 𝕜 s

theorem uniqueDiffWithinAt_convex_of_isRCLikeNormedField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [h𝕜 : IsRCLikeNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] {s : Set E} {x : E} (conv : Convex ℝ s) (hs : (interior s).Nonempty) (hx : x ∈ closure s) : UniqueDiffWithinAt 𝕜 s x

In a real or complex vector space, a convex set with nonempty interior is a set of unique differentiability.

theorem uniqueDiffOn_convex_of_isRCLikeNormedField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [h𝕜 : IsRCLikeNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] {s : Set E} (conv : Convex ℝ s) (hs : (interior s).Nonempty) : UniqueDiffOn 𝕜 s

In a real or complex vector space, a convex set with nonempty interior is a set of unique differentiability.