uniqueDiffOn_Icc

Mathlib.Analysis.Calculus.TangentCone

URI: https://scilib.ai/kg/mathlib#uniqueDiffOn_Icc

← MathLib Explorer

English

For real a < b, the closed interval [a,b] has UniqueDiffOn.

Русский

При a < b замкнутый интервал [a,b] имеет уникальную дифференцируемость.

LaTeX

$$$ \\operatorname{UniqueDiffOn}_{\\mathbb{R}}(\\mathrm{Icc}(a,b)) $$$

Lean4

theorem uniqueDiffOn_Icc {a b : ℝ} (hab : a < b) : UniqueDiffOn ℝ (Icc a b) :=
  uniqueDiffOn_convex (convex_Icc a b) <| by simp only [interior_Icc, nonempty_Ioo, hab]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru