English
The finite product of a family of sets with UniqueDiffOn has UniqueDiffOn.
Русский
Конечное произведение множества с уникальной дифференцируемостью сохраняет это свойство.
LaTeX
$$$ (\\forall i, \\operatorname{UniqueDiffOn}_{\\mathbb{k}}(s_i)) \\Rightarrow \\operatorname{UniqueDiffOn}_{\\mathbb{k}}(\\mathrm{Set.pi\\ univ\\ s}) $$$
Lean4
/-- The finite product of a family of sets of unique differentiability is a set of unique
differentiability. -/
theorem univ_pi (ι : Type*) [Finite ι] (E : ι → Type*) [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)]
(s : ∀ i, Set (E i)) (h : ∀ i, UniqueDiffOn 𝕜 (s i)) : UniqueDiffOn 𝕜 (Set.pi univ s) :=
UniqueDiffOn.pi _ _ _ _ fun i _ => h i
