condition — Mathlib

English

In a kernel fork, the leg maps compose to zero with the target arrow.

Русский

В ядровом вилке правая композиция проходима к нулю: соответствие условию Fork.

LaTeX

$$$\\forall f:\\, X\\to Y,\\ s:\\mathrm{KernelFork}(f),\\; \\mathrm{Fork.ι}\\,s\\;\\circ f = 0.$$$

Lean4

@[reassoc (attr := simp)]
theorem condition (s : KernelFork f) : Fork.ι s ≫ f = 0 := by rw [Fork.condition, HasZeroMorphisms.comp_zero]

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