English
If for each i in I, s_i has UniqueDiffWithinAt 𝕜 (x_i), then Set.pi I s has UniqueDiffWithinAt 𝕜 at x.
Русский
Если для каждого i в I множество s_i обладает уникальной дифференцируемостью в координате x_i, то произведение по индексу I обладает этой же свойством в элементе x.
LaTeX
$$$ (\\forall i \\in I, \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}}(s_i)(x_i)) \\Rightarrow \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}}(\\mathrm{Set.pi\\ I\\ s})\\; x $$$
Lean4
/-- The finite product of a family of sets of unique differentiability is a set of unique
differentiability. -/
theorem pi (ι : Type*) [Finite ι] (E : ι → Type*) [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)]
(s : ∀ i, Set (E i)) (I : Set ι) (h : ∀ i ∈ I, UniqueDiffOn 𝕜 (s i)) : UniqueDiffOn 𝕜 (Set.pi I s) := fun x hx =>
UniqueDiffWithinAt.pi _ _ _ _ _ fun i hi => h i hi (x i) (hx i hi)
