uniqueDiffOn_Iic

Mathlib.Analysis.Calculus.TangentCone

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

English

For every real a, the closed-right ray [a, ∞) has UniqueDiffOn.

Русский

Для каждого числа a на вещественной оси луч [a, ∞) имеет уникальную дифференцируемость.

LaTeX

$$$ \\operatorname{UniqueDiffOn}_{\\mathbb{R}}([a,\\infty)) $$$

Lean4

theorem uniqueDiffOn_Iic (a : ℝ) : UniqueDiffOn ℝ (Iic a) :=
  uniqueDiffOn_convex (convex_Iic a) <| by simp only [interior_Iic, nonempty_Iio]

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

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

Разделы

Аффилиация

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