over

Mathlib.CategoryTheory.Comma.Over.OverClass

URI: https://scilib.ai/kg/mathlib#CategoryTheory.OverClass.Simps.over

Lean4

/-- See Note [custom simps projection] -/
def over (X S : C) [OverClass X S] : X ⟶ S :=
  X ↘ S

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

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

Разделы

Аффилиация

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