English
If J is a small category and F: J ⥤ TopCat is a cofiltered (or empty) diagram consisting of nonempty compact Hausdorff spaces, then the inverse limit cone of F is nonempty.
Русский
Пусть J — малая категория, а F: J ⥤ TopCat задаёт кофильтрованный (или пустой) диаграмму, состоящую из непустых компактных хаусдорфовых пространств. Тогда противообратимый предел F непуст.
LaTeX
$$$\\operatorname{Nonempty}\\left(\\operatorname{TopCat.limitCone} F\\right).pt$$$
Lean4
/-- Cofiltered limits of nonempty compact Hausdorff spaces are nonempty topological spaces.
-/
theorem nonempty_limitCone_of_compact_t2_cofiltered_system (F : J ⥤ TopCat.{max v u}) [IsCofilteredOrEmpty J]
[∀ j : J, Nonempty (F.obj j)] [∀ j : J, CompactSpace (F.obj j)] [∀ j : J, T2Space (F.obj j)] :
Nonempty (TopCat.limitCone F).pt := by
classical
obtain ⟨u, hu⟩ :=
IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed (fun G => partialSections F _)
(partialSections.directed F) (fun G => partialSections.nonempty F _)
(fun G => IsClosed.isCompact (partialSections.closed F _)) fun G => partialSections.closed F _
use u
intro X Y f
let G : FiniteDiagram J := ⟨{ X, Y }, {⟨X, Y, by grind, by grind, f⟩}⟩
exact hu _ ⟨G, rfl⟩ (Finset.mem_singleton_self _)
