curry₃_obj_obj_obj_map — Mathlib

English

The map in the third component under curry3.obj.obj.obj equals the corresponding component of F

Русский

Отображение в третьем компоненте под curry3.obj.obj.obj равно соответствующему компоненту F

LaTeX

$$$\text{curry}_3.obj.obj.obj\_map : ... = F.map \langle \mathrm{id}, \mathrm{id}, f \rangle$$$

Lean4

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

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