English
If for every index type ι and every family t: ι → Set X of sets which are closed, the intersection over all i is empty, then there exists a countable subfamily whose intersection is also empty; this implies X is Lindelöf.
Русский
Если для любой индексовой семьи замкнутых подмножеств {t_i} в X с ⋂_i t_i = ∅ найдется счетное подмножество, чья общая пересечение тоже пусто, то X является Линдельфовым.
LaTeX
$$$\forall X\,[{\\text{TopologicalSpace } X}]\, (\forall \iota\, (t: \iota \to S)]\, (\\forall i, IsClosed (t(i)))\to ⋂ i, t(i) = ∅ \to \exists u: Set \iota, u.Countable \land ⋂ i\in u, t(i) = ∅)$$$
Lean4
theorem lindelofSpace_of_countable_subfamily_closed
(h :
∀ {ι : Type u} (t : ι → Set X),
(∀ i, IsClosed (t i)) → ⋂ i, t i = ∅ → ∃ u : Set ι, u.Countable ∧ ⋂ i ∈ u, t i = ∅) :
LindelofSpace X where isLindelof_univ := isLindelof_of_countable_subfamily_closed fun t => by simpa using h t
