fstKernelFork

Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.BinaryBicone.fstKernelFork

Lean4

/-- A kernel fork for the kernel of `BinaryBicone.fst`. It consists of the morphism
`BinaryBicone.inr`. -/
def fstKernelFork : KernelFork c.fst :=
  KernelFork.ofι c.inr c.inr_fst

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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