Indexed product of sets with unique differentiability property #
In this file we prove that the indexed product
of a family sets with unique differentiability property
has the same property, see UniqueDiffOn.pi and UniqueDiffOn.univ_pi.
theorem
mapsTo_tangentConeAt_pi
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{ι : Type u_2}
{E : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
{s : (i : ι) → Set (E i)}
{x : (i : ι) → E i}
[DecidableEq ι]
{i : ι}
(hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j))
:
Set.MapsTo (⇑(LinearMap.single 𝕜 E i)) (tangentConeAt 𝕜 (s i) (x i)) (tangentConeAt 𝕜 (Set.univ.pi s) x)
The tangent cone of a product contains the tangent cone of each factor.
@[deprecated mapsTo_tangentConeAt_pi (since := "2025-04-27")]
theorem
mapsTo_tangentCone_pi
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{ι : Type u_2}
{E : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
{s : (i : ι) → Set (E i)}
{x : (i : ι) → E i}
[DecidableEq ι]
{i : ι}
(hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j))
:
Set.MapsTo (⇑(LinearMap.single 𝕜 E i)) (tangentConeAt 𝕜 (s i) (x i)) (tangentConeAt 𝕜 (Set.univ.pi s) x)
Alias of mapsTo_tangentConeAt_pi.
The tangent cone of a product contains the tangent cone of each factor.
theorem
UniqueDiffWithinAt.univ_pi
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
(ι : Type u_2)
(E : ι → Type u_3)
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[Finite ι]
(s : (i : ι) → Set (E i))
(x : (i : ι) → E i)
(h : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (s i) (x i))
:
UniqueDiffWithinAt 𝕜 (Set.univ.pi s) x
theorem
UniqueDiffWithinAt.pi
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
(ι : Type u_2)
(E : ι → Type u_3)
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[Finite ι]
(s : (i : ι) → Set (E i))
(x : (i : ι) → E i)
(I : Set ι)
(h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i))
:
UniqueDiffWithinAt 𝕜 (I.pi s) x
theorem
UniqueDiffOn.pi
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
(ι : Type u_2)
(E : ι → Type u_3)
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[Finite ι]
(s : (i : ι) → Set (E i))
(I : Set ι)
(h : ∀ i ∈ I, UniqueDiffOn 𝕜 (s i))
:
UniqueDiffOn 𝕜 (I.pi s)
The finite product of a family of sets of unique differentiability is a set of unique differentiability.
theorem
UniqueDiffOn.univ_pi
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
(ι : Type u_2)
(E : ι → Type u_3)
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[Finite ι]
(s : (i : ι) → Set (E i))
(h : ∀ (i : ι), UniqueDiffOn 𝕜 (s i))
:
UniqueDiffOn 𝕜 (Set.univ.pi s)
The finite product of a family of sets of unique differentiability is a set of unique differentiability.