hasMFDerivWithinAt_univ

Mathlib.Geometry.Manifold.MFDeriv.Basic

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

← MathLib Explorer

English

A HasMFDerivWithinAt implies HasMFDerivAt when restricted to univ.

Русский

HasMFDerivWithinAt на универсе эквивалентно HasMFDerivAt.

LaTeX

$$HasMFDerivWithinAt I I' f univ x f' ↔ HasMFDerivAt I I' f x f'$$

Lean4

@[simp, mfld_simps]
theorem hasMFDerivWithinAt_univ : HasMFDerivWithinAt I I' f univ x f' ↔ HasMFDerivAt I I' f x f' := by
  simp only [HasMFDerivWithinAt, HasMFDerivAt, continuousWithinAt_univ, mfld_simps]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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