contDiff_ofLp

Mathlib.Analysis.Calculus.ContDiff.WithLp

URI: https://scilib.ai/kg/mathlib#WithLp.contDiff_ofLp

English

In the prod space, the ContDiff property holds via the prodContinuousLinearEquiv.

Русский

В произведенном пространстве свойство ContDiff держится через prodContinuousLinearEquiv.

LaTeX

$$$(prodContinuousLinearEquiv p 𝕜 E F).contDiff$$

Lean4

theorem contDiff_ofLp : ContDiff 𝕜 n (@ofLp p (E × F)) :=
  (prodContinuousLinearEquiv p 𝕜 E F).contDiff

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

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

Разделы

Аффилиация

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