yonedaEquivFst_eq

Mathlib.CategoryTheory.Comma.Presheaf.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.OverPresheafAux.YonedaCollection.yonedaEquivFst_eq

English

For p : OverArrows η s, the app component equals yonedaEquiv s when evaluated at X.

Русский

Для p : OverArrows η s, компонент приложения равен yonedaEquiv s при вычислении на X.

LaTeX

$$$\\forall p : OverArrows η s, η.app (op X) p.val = yonedaEquiv s$$$

Lean4

theorem yonedaEquivFst_eq (p : YonedaCollection F X) : p.yonedaEquivFst = yonedaEquiv p.fst :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru