curry₃_obj_obj_map_app — Mathlib

English

A simplification of the action of curry3 on a map at the first component

Русский

Упрощение действия curry3 на отображение в первом компоненте

LaTeX

$$$\text{curry}_3.obj\_map\_app\_app : ...$$$

Lean4

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

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