English
If s is Lindelöf, and p assigns a property to sets with stability under restriction and union, and every x in s has a neighborhood t in s with p(t), then p(s) holds.
Русский
Если s — множество Линдельёфа, и p — свойство над множествами, сохраняющееся при взятии подмножеств и объединений, и для каждого x∈s существует окрестность t⊆s с p(t), тогда p(s) выполняется.
LaTeX
$$$$\text{IsLindelof}(s) \Rightarrow \big( \forall p, \text{stability under restriction/union} \Rightarrow p(s) \big).$$$$
Lean4
/-- A set `s` is Lindelöf if every nontrivial filter `f` with the countable intersection
property that contains `s`, has a clusterpoint in `s`. The filter-free definition is given by
`isLindelof_iff_countable_subcover`. -/
def IsLindelof (s : Set X) :=
∀ ⦃f⦄ [NeBot f] [CountableInterFilter f], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f
