mk' — Mathlib

English

The trW condition is equivalent to the existence, for a morphism g, of a witnessing triangle with apex X and a cone Y such that P X holds; under stability under shifts, this equivalence is refined by allowing a shifted witness.

Русский

Условие trW эквивалентно существованию гомоморфизма g с треугольником-удостоверителем вершины X и конуса Y, так что P X выполняется; при устойчивости к сдвигам эквивалентность уточняется через сдвиг.

LaTeX

$$$P.trW g \\iff \\exists X,f,h,\\; \\triangle(f,g,h) \\in distTriang(C) \\land P X$$$

Lean4

theorem mk' [P.IsClosedUnderIsomorphisms]
    (hP : ∀ (T : Triangle C) (_ : T ∈ distTriang C) (_ : P T.obj₁) (_ : P T.obj₃), P T.obj₂) : P.IsTriangulatedClosed₂
    where ext₂' := by simpa only [isoClosure_eq_self] using hP

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