uniqueDiffOn_Ioi

Mathlib.Analysis.Calculus.TangentCone

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

English

For every a, the open ray (a, ∞) has UniqueDiffOn.

Русский

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

LaTeX

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

Lean4

theorem uniqueDiffOn_Ioi (a : ℝ) : UniqueDiffOn ℝ (Ioi a) :=
  isOpen_Ioi.uniqueDiffOn

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

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

Разделы

Аффилиация

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