uniqueDiffOn_univ

Mathlib.Analysis.Calculus.TangentCone

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

English

The entire space has the unique differentiability property.

Русский

Вся пространство обладает свойством уникальной дифференцируемости.

LaTeX

$$$UniqueDiffOn_{\\mathbb{k}}(\\operatorname{univ})$$$

Lean4

@[simp]
theorem uniqueDiffOn_univ : UniqueDiffOn 𝕜 (univ : Set E) := fun _ _ => uniqueDiffWithinAt_univ

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

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

Разделы

Аффилиация

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