English
If s is Lindelöf, then the complement of s belongs to any countable-intersection filter f provided that every x∈s has a neighborhood influence ensuring the complement is in f.
Русский
Если s — Линдельёфово множество, то его дополнение принадлежит любому фильтру с свойством счетного пересечения, если для каждого x∈s существует окрестность, чья дополняющая часть принадлежит этому фильтру.
LaTeX
$$$$s^c \in f \quad\text{whenever } f \text{ has } \text{CountableInterFilter} \text{ and } s\subseteq?$$$$
Lean4
/-- The complement to a Lindelöf set belongs to a filter `f` with the countable intersection
property if it belongs to each filter `𝓝 x ⊓ f`, `x ∈ s`. -/
theorem compl_mem_sets (hs : IsLindelof s) {f : Filter X} [CountableInterFilter f] (hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f) :
sᶜ ∈ f := by
contrapose! hf
simp only [notMem_iff_inf_principal_compl, compl_compl, inf_assoc] at hf ⊢
exact hs inf_le_right
