Product of sets with unique differentiability property #
In this file we prove that the product of two sets with unique differentiability property
has the same property, see UniqueDiffOn.prod.
theorem
subset_tangentConeAt_prod_left
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{s : Set E}
{y : F}
{t : Set F}
(ht : y ∈ closure t)
:
The tangent cone of a product contains the tangent cone of its left factor.
@[deprecated subset_tangentConeAt_prod_left (since := "2025-04-27")]
theorem
subset_tangentCone_prod_left
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{s : Set E}
{y : F}
{t : Set F}
(ht : y ∈ closure t)
:
Alias of subset_tangentConeAt_prod_left.
The tangent cone of a product contains the tangent cone of its left factor.
theorem
subset_tangentConeAt_prod_right
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{s : Set E}
{y : F}
{t : Set F}
(hs : x ∈ closure s)
:
The tangent cone of a product contains the tangent cone of its right factor.
@[deprecated subset_tangentConeAt_prod_right (since := "2025-04-27")]
theorem
subset_tangentCone_prod_right
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{s : Set E}
{y : F}
{t : Set F}
(hs : x ∈ closure s)
:
Alias of subset_tangentConeAt_prod_right.
The tangent cone of a product contains the tangent cone of its right factor.
theorem
UniqueDiffWithinAt.prod
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{s : Set E}
{t : Set F}
{y : F}
(hs : UniqueDiffWithinAt 𝕜 s x)
(ht : UniqueDiffWithinAt 𝕜 t y)
:
UniqueDiffWithinAt 𝕜 (s ×ˢ t) (x, y)
The product of two sets of unique differentiability at points x and y has unique
differentiability at (x, y).
theorem
UniqueDiffOn.prod
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{t : Set F}
(hs : UniqueDiffOn 𝕜 s)
(ht : UniqueDiffOn 𝕜 t)
:
UniqueDiffOn 𝕜 (s ×ˢ t)
The product of two sets of unique differentiability is a set of unique differentiability.