uniqueDiffOn_Icc_zero_one — Mathlib

English

The real closed interval [0,1] is a set of unique differentiability on the real line; i.e., it is a region of unique differentiability.

Русский

Закрытый интервал [0,1] на ℝ является областью уникальной дифференцируемости.

LaTeX

$$$\operatorname{UniqueDiffOn}_{\mathbb{R}}\bigl(\mathrm{Icc}(0,1)\bigr)$$$

Lean4

/-- The real interval `[0, 1]` is a set of unique differentiability. -/
theorem uniqueDiffOn_Icc_zero_one : UniqueDiffOn ℝ (Icc (0 : ℝ) 1) :=
  uniqueDiffOn_Icc zero_lt_one

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