continuousMultilinearCurryFin1_apply

Mathlib.Analysis.NormedSpace.Multilinear.Curry

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

← MathLib Explorer

English

Final affirmation of norm invariance under domDomCongr.

Русский

Итверждение инвариантности нормы при domDomCongr в конце.

LaTeX

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

Lean4

@[simp]
theorem continuousMultilinearCurryFin1_apply (f : G [×1]→L[𝕜] G') (x : G) :
    continuousMultilinearCurryFin1 𝕜 G G' f x = f (Fin.snoc 0 x) :=
  rfl

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

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

Разделы

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

Аффилиация

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