English
A set is Lindelöf if and only if every open cover has a countable subcover.
Русский
Множество — Линдельёфово тогда и только тогда, когда каждое открытое покрытие имеет счётное подпокрытие.
LaTeX
$$$IsLindelof(s) \iff \forall U: (ι \to Set X), (\forall i, IsOpen(U(i))) \to (s \subseteq \bigcup_i U(i)) \to \exists t \subseteq ι, t.Countable \land s \subseteq \bigcup_{i\in t} U(i).$$$
Lean4
/-- A set `s` is Lindelöf if and only if
for every family of closed sets whose intersection avoids `s`,
there exists a countable subfamily whose intersection avoids `s`. -/
theorem isLindelof_iff_countable_subfamily_closed :
IsLindelof s ↔
∀ {ι : Type u} (t : ι → Set X),
(∀ i, IsClosed (t i)) → (s ∩ ⋂ i, t i) = ∅ → ∃ u : Set ι, u.Countable ∧ (s ∩ ⋂ i ∈ u, t i) = ∅ :=
⟨fun hs ↦ hs.elim_countable_subfamily_closed, isLindelof_of_countable_subfamily_closed⟩
