snd

Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

URI: https://scilib.ai/kg/mathlib#CategoryTheory.FunctorToTypes.prod.snd

Lean4

/-- The second projection of `prod F G`, onto `G`. -/
@[simps]
def snd : prod F G ⟶ G where app _ a := a.2

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

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

Разделы

Аффилиация

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