trW_iff — Mathlib

English

The trW predicate is equivalent to the existence, for a given morphism f, of a witness triangle in distTriang(C) with apex X, such that P X holds.

Русский

Утверждается, что trW f эквивалентно существованию треугольника-удостоверителя с вершиной X и P X, если треугольник принадлежит distTriang(C).

LaTeX

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

Lean4

theorem trW_iff {X Y : C} (f : X ⟶ Y) :
    P.trW f ↔ ∃ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ X⟦(1 : ℤ)⟧) (_ : Triangle.mk f g h ∈ distTriang C), P Z := by rfl

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