initial_of_isCofiltered_pUnit — Mathlib

English

If C is cofiltered, then every functor F: C ⥤ Discrete PUnit is initial.

Русский

Если C кофильтрована, то любой функтор F: C ⥤ Discrete PUnit начален.

LaTeX

$$$[IsCofiltered(C)] \Rightarrow \forall F : C \to \mathrm{Discrete}(PUnit), \ \mathrm{Initial}(F)$$$

Lean4

/-- If `C` is cofiltered, then every functor `F : C ⥤ Discrete PUnit` is initial. -/
theorem initial_of_isCofiltered_pUnit [IsCofiltered C] (F : C ⥤ Discrete PUnit) : Initial F :=
  by
  refine initial_of_exists_of_isCofiltered F (fun _ => ?_) (fun {_} {c} _ _ => ?_)
  · use Classical.choice IsCofiltered.nonempty
    exact ⟨Discrete.eqToHom (by simp)⟩
  · use c; use 𝟙 c
    apply Subsingleton.elim

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