coproducts_of_small — Mathlib

English

If there exists a discrete J with W.colimitsOfShape(Discrete J) f and J is small, then coproducts W f holds.

Русский

Если существует дискретный J, такой что W.colimitsOfShape(Discrete J) f и J мал, тогда выполняется coproducts W f.

LaTeX

$$W.colimitsOfShape(Discrete J) f → coproducts(W,f) [Small J]$$

Lean4

theorem coproducts_of_small {X Y : C} (f : X ⟶ Y) {J : Type w'} (hf : W.colimitsOfShape (Discrete J) f) [Small.{w} J] :
    coproducts.{w} W f := by
  rw [coproducts_iff]
  refine ⟨Shrink J, ?_⟩
  rwa [← W.colimitsOfShape_eq_of_equivalence (Discrete.equivalence (equivShrink.{w} J))]

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