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} [Semiring 𝕜] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousAdd (E i)] [∀ (i : ι), ContinuousConstSMul 𝕜 (E i)] {s : (i : ι) → Set (E i)} {x : (i : ι) → E i} [DecidableEq ι] {i : ι} (hi : ∀ (j : ι), j ≠ i → x j ∈ closure (s j)) : Set.MapsTo (Pi.single 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.

theorem UniqueDiffWithinAt.univ_pi {𝕜 : Type u_1} [Semiring 𝕜] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousAdd (E i)] [∀ (i : ι), ContinuousConstSMul 𝕜 (E i)] {s : (i : ι) → Set (E i)} {x : (i : ι) → E i} (h : ∀ (i : ι), UniqueDiffWithinAt 𝕜 (s i) (x i)) : UniqueDiffWithinAt 𝕜 (Set.univ.pi s) x

theorem UniqueDiffOn.univ_pi {𝕜 : Type u_1} [Semiring 𝕜] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousAdd (E i)] [∀ (i : ι), ContinuousConstSMul 𝕜 (E i)] {s : (i : ι) → Set (E i)} (h : ∀ (i : ι), UniqueDiffOn 𝕜 (s i)) : UniqueDiffOn 𝕜 (Set.univ.pi s)

The product of a family of sets of unique differentiability is a set of unique differentiability.

theorem UniqueDiffWithinAt.pi {𝕜 : Type u_1} [DivisionSemiring 𝕜] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [TopologicalSpace 𝕜] [(nhdsWithin 0 {0}ᶜ).NeBot] [(i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousAdd (E i)] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {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} [DivisionSemiring 𝕜] {ι : Type u_2} {E : ι → Type u_3} [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [TopologicalSpace 𝕜] [(nhdsWithin 0 {0}ᶜ).NeBot] [(i : ι) → TopologicalSpace (E i)] [∀ (i : ι), ContinuousAdd (E i)] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] {s : (i : ι) → Set (E i)} {I : Set ι} (h : ∀ i ∈ I, UniqueDiffOn 𝕜 (s i)) : UniqueDiffOn 𝕜 (I.pi s)

The product of a family of sets of unique differentiability is a set of unique differentiability.