English
Let F be a functor from a small category J to TopCat with each space F(j) Hausdorff. For any finite diagram G and any finite set H of arrows in G, the collection of partial sections (compatible choices of points over the objects indexed by G that respect the arrows in H) forms a closed subset in the product topology over the objects in G.
Русский
Пусть F: J ⥤ TopCat, где пространства F(j) являются хаусдорфовыми. Для любой конечной диаграммы G и любого конечного множества стрелок H диаграммы G множество частичных секций является замкнутым подмножеством в произведении пространств по объектам G.
LaTeX
$$$\\operatorname{IsClosed}\\bigl( \\mathrm{partialSections}(F,H) \\bigr)$$$
Lean4
theorem closed [∀ j : J, T2Space (F.obj j)] {G : Finset J} (H : Finset (FiniteDiagramArrow G)) :
IsClosed (partialSections F H) :=
by
have : partialSections F H = ⋂ (f : FiniteDiagramArrow G) (_ : f ∈ H), {u | F.map f.2.2.2.2 (u f.1) = u f.2.1} :=
by
ext1
simp only [Set.mem_iInter, Set.mem_setOf_eq]
rfl
rw [this]
apply isClosed_biInter
intro f _
apply isClosed_eq <;> fun_prop
