English
If P is stable under shifts, then trW f is equivalent to the existence of a witness with apex X, and with the shifts adjusted by the inverse/forward shift.
Русский
Если P устойчиво к сдвигам, то trW f эквивалентно существованию свидетеля с вершиной X и смещениями, скорректированными инверсным/прямым сдвигом.
LaTeX
$$$[P.IsStableUnderShift]+ trW_iff' g : P.trW g \\iff \\exists X,f,h, (f,g,h) \\in distTriang(C) \\land P X$$$
Lean4
theorem trW_iff' [P.IsStableUnderShift ℤ] {Y Z : C} (g : Y ⟶ Z) :
P.trW g ↔ ∃ (X : C) (f : X ⟶ Y) (h : Z ⟶ X⟦(1 : ℤ)⟧) (_ : Triangle.mk f g h ∈ distTriang C), P X :=
by
rw [P.trW_iff]
constructor
· rintro ⟨Z, g, h, H, mem⟩
exact ⟨_, _, _, inv_rot_of_distTriang _ H, P.le_shift (-1) _ mem⟩
· rintro ⟨Z, g, h, H, mem⟩
exact ⟨_, _, _, rot_of_distTriang _ H, P.le_shift 1 _ mem⟩
