English
If s has unique differentiability and t is open, then s ∩ t has unique differentiability.
Русский
Если у множества s есть уникальная дифференцируемость, а множество t открыто, то s ∩ t также имеет уникальную дифференциируемость.
LaTeX
$$$ \\operatorname{UniqueDiffOn}_{\\mathbb{k}}(s) \\Rightarrow \\operatorname{IsOpen}(t) \\Rightarrow \\operatorname{UniqueDiffOn}_{\\mathbb{k}}(s \\cap t) $$$
Lean4
theorem inter (hs : UniqueDiffOn 𝕜 s) (ht : IsOpen t) : UniqueDiffOn 𝕜 (s ∩ t) := fun x hx =>
(hs x hx.1).inter (IsOpen.mem_nhds ht hx.2)