uniqueDiffOn_Ioo — Mathlib

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

Похожие утверждения