nonempty_of_nonempty_colimit — Mathlib

English

If the colimit of F is nonempty, then the index category J is nonempty.

Русский

Если колимит F непуст, то индексное множество J непустое.

LaTeX

$$$$ \text{Nonempty}(\operatorname{colimit} F) \Rightarrow \text{Nonempty}(J). $$$$

Lean4

/-- If a colimit is nonempty, also its index category is nonempty. -/
theorem nonempty_of_nonempty_colimit {F : J ⥤ Type u} [HasColimit F] : Nonempty (colimit F) → Nonempty J :=
  Nonempty.map <| Sigma.fst ∘ Quot.out ∘ (colimitEquivColimitType F).toFun

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