curry₃_map_app_app_app — Mathlib

English

Let F, G be functors C1 × C2 × C3 → E and f : F ⟶ G. Then the threefold curry map of f, evaluated at triples (X1, X2, X3), equals the original component of f at ⟨X1, X2, X3⟩.

Русский

Пусть F, G : C1 × C2 × C3 ⥤ E и f : F ⟶ G. Тогда каррированное преобразование f тройного размера, взятое на тройке аргументов (X1, X2, X3), совпадает с компонентом f в точке ⟨X1, X2, X3⟩.

LaTeX

$$$$ (((\\operatorname{curry}_3.map\,f).app X_1).app X_2).app X_3 \;=\; f.\\!app\\langle X_1, X_2, X_3\\rangle. $$$$

Lean4

@[simp]
theorem curry₃_map_app_app_app {F G : C₁ × C₂ × C₃ ⥤ E} (f : F ⟶ G) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) :
    (((curry₃.map f).app X₁).app X₂).app X₃ = f.app ⟨X₁, X₂, X₃⟩ :=
  rfl

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