uncurry0_apply

Mathlib.Analysis.NormedSpace.Multilinear.Curry

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

English

For a zero-argument multilinear map, uncurry0 applied to curry0 yields the original map: uncurry0 𝕜 G (f.curry0) = f.

Русский

Для нулевой размерности отображения uncurry0 𝕜 G (f.curry0) = f.

LaTeX

$$$\\mathrm{uncurry0}\\,\\,𝕜\\,G\\,(f.\\text{curry0}) = f$$$

Lean4

@[simp]
theorem uncurry0_apply (x : G') (m : Fin 0 → G) : ContinuousMultilinearMap.uncurry0 𝕜 G x m = x :=
  rfl

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

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

Разделы

Аффилиация

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