uliftYonedaEquiv_comp — Mathlib

English

For X in C and F,G in Cᵒᵖ ⥤ Type, and α: uliftYoneda.obj X ⟶ F, β: F ⟶ G, uliftYonedaEquiv(α ≫ β) = β.app _ (uliftYonedaEquiv α).

Русский

Для X в C и F,G в Cᵒᵖ ⥤ Type, α: uliftYoneda.obj X ⟶ F, β: F ⟶ G: uliftYonedaEquiv(α ≫ β) = β.app _ (uliftYonedaEquiv α).

LaTeX

$$$uliftYonedaEquiv.{w} (\alpha ≫ \beta) = \beta.app _ (uliftYonedaEquiv.{w} \alpha)$$$

Lean4

theorem uliftYonedaEquiv_comp {X : C} {F G : Cᵒᵖ ⥤ Type max w v₁} (α : uliftYoneda.{w}.obj X ⟶ F) (β : F ⟶ G) :
    uliftYonedaEquiv.{w} (α ≫ β) = β.app _ (uliftYonedaEquiv α) :=
  rfl

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