English
For any P closed under isomorphisms, P.trW T.mor₁ holds iff P(T.obj₃) holds for T distinguished in distTriang.
Русский
Для P, замкнутого относительно изоморфизмов, P.trW T.mor₁ эквивалентно P(T.obj₃) для дискриминированного T.
LaTeX
$$$[P.IsClosedUnderIsomorphisms] \\Rightarrow (T \\in \\mathrm{distTriang}\\, C) \\to (P.trW T.mor₁ \\iff P(T.obj₃))$$$
Lean4
theorem trW_iff_of_distinguished [P.IsClosedUnderIsomorphisms] (T : Triangle C) (hT : T ∈ distTriang C) :
P.trW T.mor₁ ↔ P T.obj₃ := by
constructor
· rintro ⟨Z, g, h, hT', mem⟩
obtain ⟨e, _⟩ := exists_iso_of_arrow_iso _ _ hT' hT (Iso.refl _)
exact P.prop_of_iso (Triangle.π₃.mapIso e) mem
· intro h
exact ⟨_, _, _, hT, h⟩