instHasKernelFst

Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

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

English

There exists a kernel of biprod.fst, i.e., HasKernel (biprod.fst).

Русский

Существует ядро для biprod.fst, то есть HasKernel (biprod.fst).

LaTeX

$$$\text{HasKernel}(\mathrm{biprod.fst})$$$

Lean4

instance : HasKernel (biprod.fst : X ⊞ Y ⟶ X) :=
  HasLimit.mk ⟨_, biprod.isKernelFstKernelFork X Y⟩

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

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

Разделы

Аффилиация

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