curry_apply

Mathlib.Topology.Homotopy.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousMap.Homotopy.curry_apply

English

The curry of F at 0 equals f0.

Русский

Карри-гомотопия F при 0 равна f0.

LaTeX

$$$F\text{.curry}(0) = f_0$$$

Lean4

@[simp]
theorem curry_apply (F : Homotopy f₀ f₁) (t : I) (x : X) : F.curry t x = F (t, x) :=
  rfl

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

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

Разделы

Аффилиация

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