curry_obj_injective — Mathlib

English

If two curries of functors from Prod C D to E are equal, then the original functors are equal: curry.obj F1 = curry.obj F2 implies F1 = F2.

Русский

Если две каррированные функции F1, F2 равны, то сами F1 и F2 равны: curry.obj F1 = curry.obj F2 ⇒ F1 = F2.

LaTeX

$$$\text{curry.obj}$ is injective on morphisms: if $\operatorname{curry.obj} F_1 = \operatorname{curry.obj} F_2$ then $F_1 = F_2$.$$

Lean4

theorem curry_obj_injective {F₁ F₂ : C × D ⥤ E} (h : curry.obj F₁ = curry.obj F₂) : F₁ = F₂ := by
  rw [← uncurry_obj_curry_obj F₁, ← uncurry_obj_curry_obj F₂, h]

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