English
Let X be a Hausdorff topological space and s be a finite index set. For a family t(i) of subsets of X, if every t(i) with i in s is retrocompact in X, then the intersection over all i in s of t(i) is retrocompact.
Русский
Пусть X — пространство топологии Хаусдорфа и s конечно. Для семейства t(i) подмножеств X, если для каждого i ∈ s множество t(i) ретрокомпактно в X, то пересечение по i ∈ s множеств t(i) ретрокомпактно.
LaTeX
$$$(\\forall i \\in s,\\ IsRetrocompact(t(i))) \\rightarrow IsRetrocompact\\left(\\bigcap_{i \\in s} t(i)\\right)$$$
Lean4
theorem finsetInf {ι : Type*} {s : Finset ι} {t : ι → Set X} (ht : ∀ i ∈ s, IsRetrocompact (t i)) :
IsRetrocompact (s.inf t) := by
induction s using Finset.cons_induction with
| empty => simp
| cons i s ih hi =>
rw [Finset.inf_cons]
exact (ht _ <| by simp).inter <| hi <| Finset.forall_of_forall_cons ht
