uncurry0_curry0

Mathlib.Analysis.NormedSpace.Multilinear.Curry

URI: https://scilib.ai/kg/mathlib#ContinuousMultilinearMap.uncurry0_curry0

English

Reiterates that applying a relabelling of indices via domDomCongr preserves the operator norm.

Русский

Повторение того, что перестановка индексов через domDomCongr сохраняет норму оператора.

LaTeX

$$$\\|domDomCongr\\;\\sigma\\;f\\| = \\|f\\|$$$

Lean4

theorem uncurry0_curry0 (f : G [×0]→L[𝕜] G') : ContinuousMultilinearMap.uncurry0 𝕜 G f.curry0 = f := by simp

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

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

Разделы

Аффилиация

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