asOver

Mathlib.CategoryTheory.Comma.Over.OverClass

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

Lean4

/-- Bundle `X` with an `OverClass X S` instance into `Over S`. -/
@[simps! hom left]
def asOver [OverClass X S] : Over S :=
  Over.mk (X ↘ S)

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

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

Разделы

Аффилиация

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