coyonedaEquiv_symm_app_apply — Mathlib

English

The symm of coyonedaEquiv applied to x has a computable formula: (coyonedaEquiv.symm x).app Y f = F.map f x.

Русский

Обратимое приложение coyonedaEquiv к x имеет формулу: (coyonedaEquiv.symm x).app Y f = F.map f x.

LaTeX

$$$(coyonedaEquiv.symm x).app Y f = F.map f x$$$

Lean4

@[simp]
theorem coyonedaEquiv_symm_app_apply {X : C} {F : C ⥤ Type v₁} (x : F.obj X) (Y : C) (f : X ⟶ Y) :
    (coyonedaEquiv.symm x).app Y f = F.map f x :=
  rfl

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