instIsFilteredI — Mathlib

English

A concrete equality ties the two isColimit presentations via ι₁, ι₂ and ϕ.

Русский

Конкретное равенство связывает две индуктивные презентации через ι₁, ι₂ и ϕ.

LaTeX

$$$f = \mathrm{IsColimit.map}(\mathrm{isColimit}_1\,f\,g\,P_1\,P_2)\; (\mathrm{Cocone.mk}\ B\ (\iota_2\,f\,g\,P_1\,P_2))\; (\mathrm{whiskerRight}(\varphi\,f\,g\,P_1\,P_2)\; \mathrm{yoneda})$$$

Lean4

instance {A B : Cᵒᵖ ⥤ Type v₁} {f g : A ⟶ B} (P : IndParallelPairPresentation f g) : IsFiltered P.I :=
  P.hI

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