uniqueMDiffOn

Mathlib.Geometry.Manifold.MFDeriv.Basic

URI: https://scilib.ai/kg/mathlib#IsOpen.uniqueMDiffOn

English

If s is open, then the unique MDiffOn property holds for s.

Русский

Если s открыто, то для s выполняется свойство уникальной MDiffOn.

LaTeX

$$IsOpen.uniqueMDiffOn (hs := _)$$

Lean4

theorem uniqueMDiffOn (hs : IsOpen s) : UniqueMDiffOn I s := fun _x hx => hs.uniqueMDiffWithinAt hx

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

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

Разделы

Аффилиация

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