initial_iff_isCofiltered_costructuredArrow

English

For any F : C → D, with C cofiltered-or-empty, Initial F holds iff CostructuredArrow F d is cofiltered for all d ∈ D.

Русский

Для любого F : C → D, если C — кофильтрована или пустая, то Initial F верно тогда и только тогда, когда CostructuredArrow F d кофильтрована для всех d ∈ D.

LaTeX

$$Initial F ↔ ∀ d, IsCofiltered (CostructuredArrow F d)$$

Lean4

/-- If `C` is cofiltered, then `F : C ⥤ D` is initial if and only if `CostructuredArrow F d` is
cofiltered for all `d : D`. -/
theorem initial_iff_isCofiltered_costructuredArrow [IsCofilteredOrEmpty C] :
    Initial F ↔ ∀ d, IsCofiltered (CostructuredArrow F d) :=
  by
  refine ⟨?_, fun h => initial_of_isCofiltered_costructuredArrow F⟩
  rw [initial_iff_of_isCofiltered]
  exact fun h => isCofiltered_costructuredArrow_of_isCofiltered_of_exists F h.1 h.2

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