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}
:
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.