curry0_norm

Mathlib.Analysis.NormedSpace.Multilinear.Curry

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

English

Again asserts that the norm is invariant under index relabelling by domDomCongr.

Русский

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

LaTeX

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

Lean4

theorem curry0_norm (f : G [×0]→L[𝕜] G') : ‖f.curry0‖ = ‖f‖ := by simp

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

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

Разделы

Аффилиация

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