English
The family of partial sections forms a directed superset: for any two finite diagrams, their union diagram provides an inclusion of partial sections.
Русский
Семейство частичных секций образует направленный superset: для любых двух конечных диаграмм их объединение задаёт включение частичных секций.
LaTeX
$$$ \text{Directed Superset }(\mathrm{partialSections}) :\forall A,B, \mathrm{partialSections}(F,A) \subseteq \mathrm{partialSections}(F,A\sqcup B) \land \mathrm{partialSections}(F,B) \subseteq \mathrm{partialSections}(F,A\sqcup B) $$$
Lean4
theorem nonempty [IsCofilteredOrEmpty J] [h : ∀ j : J, Nonempty (F.obj j)] {G : Finset J}
(H : Finset (FiniteDiagramArrow G)) : (partialSections F H).Nonempty := by
classical
cases isEmpty_or_nonempty J
· exact ⟨isEmptyElim, fun {j} => IsEmpty.elim' inferInstance j.1⟩
haveI : IsCofiltered J := ⟨⟩
use fun j : J => if hj : j ∈ G then F.map (IsCofiltered.infTo G H hj) (h (IsCofiltered.inf G H)).some else (h _).some
rintro ⟨X, Y, hX, hY, f⟩ hf
dsimp only
rwa [dif_pos hX, dif_pos hY, ← comp_app, ← F.map_comp, @IsCofiltered.infTo_commutes _ _ _ G H]
