English
The universal finite product preserves unique differentiability: Set.pi univ s has UniqueDiffOn 𝕜 whenever each s_i has UniqueDiffOn 𝕜.
Русский
Единственный для всех элементов конечного индекса сохраняется уникальная дифференцируемость: Set.pi univ s имеет UniqueDiffOn 𝕜 при условии, что для каждого i выполнено UniqueDiffOn 𝕜 (s_i).
LaTeX
$$$ (\\forall i, \\operatorname{UniqueDiffOn}_{\\mathbb{k}}(s_i)) \\Rightarrow \\operatorname{UniqueDiffOn}_{\\mathbb{k}}(\\mathrm{Set.pi\\ univ\\, s}) $$$
Lean4
theorem pi (ι : Type*) [Finite ι] (E : ι → Type*) [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)]
(s : ∀ i, Set (E i)) (x : ∀ i, E i) (I : Set ι) (h : ∀ i ∈ I, UniqueDiffWithinAt 𝕜 (s i) (x i)) :
UniqueDiffWithinAt 𝕜 (Set.pi I s) x := by
classical
rw [← Set.univ_pi_piecewise_univ]
refine UniqueDiffWithinAt.univ_pi ι E _ _ fun i => ?_
by_cases hi : i ∈ I <;> simp [*, uniqueDiffWithinAt_univ]
