contDiff_toLp

Mathlib.Analysis.Calculus.ContDiff.WithLp

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

English

The map toLp from E×F to PiLp p is ContDiff.

Русский

Отображение toLp: E×F → PiLp p является ContDiff.

LaTeX

$$$ ContDiff 𝕜 n (WithLp.toLp p) $$$

Lean4

theorem contDiff_toLp : ContDiff 𝕜 n (@toLp p (E × F)) :=
  (prodContinuousLinearEquiv p 𝕜 E F).symm.contDiff

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

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

Разделы

Аффилиация

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