English
Under the standard Snake Lemma hypotheses, the computed Snake map δ' coincides with the connecting morphism δ when evaluated on x with the corresponding y and z satisfying f2(y) = ι3(x) and g1(z) = i2(y). Hence δ'(x) = π1(z).
Русский
При обычных условиях змейки δ' совпадает с связующим отображением δ на элементе x при наличии соответствующих y и z, удовлетворяющих f2(y) = ι3(x) и g1(z) = i2(y); следовательно δ'(x) = π1(z).
LaTeX
$$$\forall x\in K_3,\forall y,z\; (f_2(y)=\iota_3(x)\land g_1(z)=i_2(y))\Rightarrow \delta'(x)=\pi_1(z).$$$
Lean4
theorem δ'_eq (hf₂ : Surjective f₂) (hg₁ : Injective g₁) (x : K₃) (y) (hy : f₂ y = ι₃ x) (z) (hz : g₁ z = i₂ y) :
δ' i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ ι₃ hι₃ π₁ hπ₁ hf₂ hg₁ x = π₁ z :=
SnakeLemma.δ_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ‹_› ‹_› _ ‹_›
