app_one

Mathlib.CategoryTheory.Limits.Shapes.Kernels

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

English

At the kernel fork, the projection corresponding to the first leg evaluated at the distinguished point is zero.

Русский

В ядровом вилке проекция, соответствующая первой ножке, в точке, отличительной, равна нулю.

LaTeX

$$$\\forall s:\\mathrm{KernelFork}(f),\\; s.\\pi_{\\mathrm{one}} = 0.$$$

Lean4

theorem app_one (s : KernelFork f) : s.π.app one = 0 := by simp

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

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

Разделы

Аффилиация

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