English
If P.IsStableUnderShift and T is distinguished with T.hT in distTriang C, then P.trW T.mor₂ whenever P T.obj₁ holds.
Русский
Пусть P.IsStableUnderShift, и T — дискриминированный треугольник с T.hT ∈ distTriang C; если P(T.obj₁), то P.trW(T.mor₂).
LaTeX
$$$\\forall {\\mathcal C}\, [\\text{Category } \\mathcal C], [\\text{HasZeroObject } \\mathcal C], [\\text{HasShift } \\mathcal C \\mathbb{Z}], [\\text{Pretriangulated } \\mathcal C], (P : \\mathrm{ObjectProperty}\\, \\mathcal C) [P.IsStableUnderShift \\mathbb Z] \\,\\to \\\\forall {T : \\mathrm{Triangle}\\, \\mathcal C}, T \\in \\mathrm{distTriang}\\, \\mathcal C \\,\\to P(T.obj_1) \\to P\\,\\mathrm{trW}\\, T.mor_2.$$$
Lean4
theorem mk' [P.IsStableUnderShift ℤ] {T : Triangle C} (hT : T ∈ distTriang C) (h : P T.obj₁) : P.trW T.mor₂ :=
by
rw [trW_iff']
exact ⟨_, _, _, hT, h⟩
