English
Let a and b be real numbers with a < b. Then the open interval Ioo(a, b) is a set of unique differentiability on the real line; in particular every point of Ioo(a, b) is a point of unique differentiability for the ambient space.
Русский
Пусть a, b ∈ ℝ и a < b. Тогда открытый интервал Ioo(a, b) является множеством уникальной дифференцируемости на ℝ; то есть любая точка Ioo(a, b) — точка уникальной дифференциации относительно этого множества.
LaTeX
$$$\operatorname{UniqueDiffOn}_{\mathbb{R}}\bigl(\mathrm{Ioo}(a,b)\bigr)$$$
Lean4
theorem uniqueDiffOn_Ioo (a b : ℝ) : UniqueDiffOn ℝ (Ioo a b) :=
isOpen_Ioo.uniqueDiffOn