initial_of_isCofiltered_costructuredArrow

English

If CostructuredArrow F d is filtered for all d, then F is initial.

Русский

Если CostructuredArrow F d фильтрована для всех d, тогда F начальна (Initial).

LaTeX

$$$\\forall d, \\mathrm{IsFiltered}(\\mathrm{CostructuredArrow}\\, F\\, d) \\Rightarrow \\mathrm{Initial}(F)$$$

Lean4

/-- If `CostructuredArrow F d` is filtered for any `d : D`, then `F : C ⥤ D` is initial. This is
simply because cofiltered categories are connected. More profoundly, the converse is also true
if `C` is cofiltered, see `initial_iff_isCofiltered_costructuredArrow`. -/
theorem initial_of_isCofiltered_costructuredArrow [∀ d, IsCofiltered (CostructuredArrow F d)] : Initial F where
  out _ := IsCofiltered.isConnected _

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