English
If s is Lindelöf and for every x in s there exists t⊆s with t^c ∈ f, then s^c ∈ f for a countable-intersection filter f.
Русский
Если s/Lindelöf и для каждого x∈s существует t⊆s с t^c ∈ f, то s^c ∈ f для фильтра с счетным пересечением.
LaTeX
$$$$\text{IsLindelof}(s) \Rightarrow s^c \in f$$ under the CountableInterFilter condition.$$
Lean4
/-- The complement to a Lindelöf set belongs to a filter `f` with the countable intersection
property if each `x ∈ s` has a neighborhood `t` within `s` such that `tᶜ` belongs to `f`. -/
theorem compl_mem_sets_of_nhdsWithin (hs : IsLindelof s) {f : Filter X} [CountableInterFilter f]
(hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f) : sᶜ ∈ f :=
by
refine hs.compl_mem_sets fun x hx ↦ ?_
rw [← disjoint_principal_right, disjoint_right_comm, (basis_sets _).disjoint_iff_left]
exact hf x hx
