π_liftedConeElement' — Mathlib

English

If F creates colimits, and D has all colimits, then C has all colimits.

Русский

Если F создаёт колимиты, и D имеет все колимиты, то C имеет все колимиты.

LaTeX

$$$[\text{CreatesColimitsOfSize } F] \wedge [\text{HasColimitsOfSize } D] \Rightarrow [\text{HasColimitsOfSize } C]$$$

Lean4

@[simp]
theorem π_liftedConeElement' (i : I) : limit.π ((F ⋙ π A) ⋙ A) i (liftedConeElement' F) = (F.obj i).2 :=
  Types.Limit.π_mk _ _ _ _

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