English
In any finite collection of objects O in a cofiltered category, there exists an object S and morphisms S → X for every X ∈ O.
Русский
В любой конечной подмножестве объектов O в кофильтрованной категории существует объект S и морфизмы S → X для каждого X ∈ O.
LaTeX
$$$\forall O \subseteq \mathrm{Ob}(C),\; O \text{ finite } \Rightarrow \exists S \in \mathrm{Ob}(C), \forall X \in O\; \exists f: S \to X$$$
Lean4
/-- Any finite collection of objects in a cofiltered category has an object "to the left".
-/
theorem inf_objs_exists (O : Finset C) : ∃ S : C, ∀ {X}, X ∈ O → Nonempty (S ⟶ X) := by
classical
induction O using Finset.induction with
| empty => exact ⟨Classical.choice IsCofiltered.nonempty, by simp⟩
| insert X O' nm h =>
obtain ⟨S', w'⟩ := h
use min X S'
rintro Y mY
obtain rfl | h := eq_or_ne Y X
· exact ⟨minToLeft _ _⟩
· exact ⟨minToRight _ _ ≫ (w' (Finset.mem_of_mem_insert_of_ne mY h)).some⟩
