English
IsLindelöf s if and only if for every family (t_i) of closed sets, if s ∩ ⋂ t_i = ∅ then there exists a countable subfamily with empty intersection.
Русский
IsLindelöf s тогда и только тогда, когда для любой семьи закрытых множеств (t_i), если s ⊓ ⋂ t_i = ∅, существует счётная подподборка с пустым пересечением.
LaTeX
$$$IsLindelof(s) \iff \\ ∀ {t_i}, (∀ i, IsClosed(t_i)) → (s \cap \bigcap_i t_i) = \emptyset → ∃ u \subseteq I, u.Countable ∧ (s ∩ ∩_{i∈u} t_i) = ∅.$$$
Lean4
/-- To show that a Lindelöf set intersects the intersection of a family of closed sets,
it is sufficient to show that it intersects every countable subfamily. -/
theorem inter_iInter_nonempty {ι : Type v} (hs : IsLindelof s) (t : ι → Set X) (htc : ∀ i, IsClosed (t i))
(hst : ∀ u : Set ι, u.Countable ∧ (s ∩ ⋂ i ∈ u, t i).Nonempty) : (s ∩ ⋂ i, t i).Nonempty :=
by
contrapose! hst
rcases hs.elim_countable_subfamily_closed t htc hst with ⟨u, ⟨_, husub⟩⟩
exact ⟨u, fun _ ↦ husub⟩
