inl_desc — Mathlib

English

For a pushout cocone t with ht an IsColimit, the map inl t, followed by the universal desc ht h k w, equals h.

Русский

Для кони PushoutCocone t и ht — IsColimit, композиция inl t с desc ht h k w равна h.

LaTeX

$$inl t ≫ IsColimit.desc ht h k w = h$$

Lean4

@[reassoc (attr := simp)]
theorem inl_desc {t : PushoutCocone f g} (ht : IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W) (w : f ≫ h = g ≫ k) :
    inl t ≫ IsColimit.desc ht h k w = h :=
  ht.fac _ _

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