English
For a finite index set ι, if each s_i has UniqueDiffWithinAt, then the universal pi-product over all indices has UniqueDiffWithinAt.
Русский
Для конечного множества индексов ι, если для каждого i множество s_i имеет уникальную дифференцируемость, то произведение по всем i имеет уникальную дифференцируемость.
LaTeX
$$$ (\\forall i, \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}}(s_i)) \\Rightarrow \\operatorname{UniqueDiffWithinAt}_{\\mathbb{k}}(\\mathrm{Set.univ.pi}\\, s) $$$
Lean4
/-- In a real vector space, a convex set with nonempty interior is a set of unique
differentiability. -/
theorem uniqueDiffOn_convex {s : Set G} (conv : Convex ℝ s) (hs : (interior s).Nonempty) : UniqueDiffOn ℝ s :=
fun _ xs => uniqueDiffWithinAt_convex conv hs (subset_closure xs)
