iff_cocone_nonempty — Mathlib

English

IsFiltered C holds if and only if every finite diagram in C has a cocone.

Русский

IsFiltered C истина тогда и только тогда, когда каждая конечная диаграмма в C имеет кокон.

LaTeX

$$$\\operatorname{IsFiltered}(C) \\iff \\forall J [SmallCategory J] [FinCategory J] (F : J \\to C), \\operatorname{Nonempty}(\\operatorname{Cocone}(F)).$$$

Lean4

/-- For every universe `w`, `C` is filtered if and only if every finite diagram in `C` with shape
in `w` admits a cocone. -/
theorem iff_cocone_nonempty :
    IsFiltered C ↔ ∀ {J : Type w} [SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F) :=
  ⟨fun _ _ _ _ F => cocone_nonempty F, of_cocone_nonempty C⟩

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