mk' — Mathlib

English

The trW relation is equivalent to the existence, for any morphism f: X→Y, of a witness triangle with apex Z and a morphism h: Z→X[1] such that the triangle is distinguished and P Z holds.

Русский

Связь trW эквивалентна существованию треугольника-удостоверителя с вершиной Z и гомоморфизмом h: Z→X[1], при котором треугольник выделен и выполняется свойство P Z.

LaTeX

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

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

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