apply_zero_uncurry0

Mathlib.Analysis.NormedSpace.Multilinear.Curry

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

← MathLib Explorer

English

For any x in G', the norm of uncurry0 𝕜 G x equals the norm of x: ∥uncurry0 𝕜 G x∥ = ∥x∥.

Русский

Для любого x из G' выполняется ∥uncurry0 𝕜 G x∥ = ∥x∥.

LaTeX

$$$\\|\\mathrm{uncurry0}\\,\\ 𝕜\\,G\\,x\\| = \\|x\\|$$$

Lean4

@[simp]
theorem apply_zero_uncurry0 (f : G [×0]→L[𝕜] G') {x : Fin 0 → G} : ContinuousMultilinearMap.uncurry0 𝕜 G (f x) = f :=
  by
  ext m
  simp [Subsingleton.elim x m]

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

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

Разделы

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

Аффилиация

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