trW_iff_of_distinguished — Mathlib

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⟩

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