fst_of_isColimit — Mathlib

English

For a binary bicone X ⊞ Y with a Colimit structure, the first projection fib is equal to the descent along the binary cofan built from id_X and 0.

Русский

Для бинарного биконуса X ⊞ Y, имеющего колимитную структуру, первый проекции соответствует разложению по бинарному кофану, построенному из id_X и 0.

LaTeX

$$$t.fst = ht.desc (BinaryCofan.mk (id_X) 0)$$$

Lean4

theorem fst_of_isColimit {X Y : C} {t : BinaryBicone X Y} (ht : IsColimit t.toCocone) :
    t.fst = ht.desc (BinaryCofan.mk (𝟙 X) 0) :=
  by
  apply ht.uniq (BinaryCofan.mk (𝟙 X) 0)
  rintro ⟨⟨⟩⟩ <;> simp

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