iff_cone_nonempty — Mathlib

English

IsCofiltered iff every finite diagram admits a cone.

Русский

Кофильтрованность эквивалентна тому, что каждый конечный диаграмма допускает конус.

LaTeX

$$$\mathrm{IsCofiltered} C \iff \forall J,[SmallCategory J][FinCategory J]\; (F: J \to C) \Rightarrow \mathrm{Cone}\,F\text{ nonempty}$$$

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_cone_nonempty :
    IsCofiltered C ↔ ∀ {J : Type w} [SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F) :=
  ⟨fun _ _ _ _ F => cone_nonempty F, of_cone_nonempty C⟩

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