uniqueDiffOn_Iio

Mathlib.Analysis.Calculus.TangentCone

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

English

For every a, the closed-down ray (-∞, a] has UniqueDiffOn.

Русский

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

LaTeX

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

Lean4

theorem uniqueDiffOn_Iio (a : ℝ) : UniqueDiffOn ℝ (Iio a) :=
  isOpen_Iio.uniqueDiffOn

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

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

Разделы

Аффилиация

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