English
Let f be a filter with the countable intersection property, finer than the principal filter on a Lindelöf set s. If t is open and every x in s that is a cluster point of f must lie in t, then t belongs to f.
Русский
Пусть f — фильтр с свойством счётного пересечения, который более тонкий чем принци́пал фильтр на множестве Линдельёфа s. Если t открыто и для каждого x∈s, cluster-point(x,f) ⇒ x∈t, то t ∈ f.
LaTeX
$$$f\text{ имеет свойство CountableInterFilter} \land f \le 𝓟(s) \land IsOpen(t) \land (\forall x\in s, ClusterPt(x,f) \Rightarrow x\in t) \Rightarrow t \in f.$$$
Lean4
/-- A filter with the countable intersection property that is finer than the principal filter on
a Lindelöf set `s` contains any open set that contains all clusterpoints of `s`. -/
theorem adherence_nhdset {f : Filter X} [CountableInterFilter f] (hs : IsLindelof s) (hf₂ : f ≤ 𝓟 s) (ht₁ : IsOpen t)
(ht₂ : ∀ x ∈ s, ClusterPt x f → x ∈ t) : t ∈ f :=
(eq_or_neBot _).casesOn mem_of_eq_bot fun _ ↦
let ⟨x, hx, hfx⟩ := @hs (f ⊓ 𝓟 tᶜ) _ _ <| inf_le_of_left_le hf₂
have : x ∈ t := ht₂ x hx hfx.of_inf_left
have : tᶜ ∩ t ∈ 𝓝[tᶜ] x := inter_mem_nhdsWithin _ (ht₁.mem_nhds this)
have A : 𝓝[tᶜ] x = ⊥ := empty_mem_iff_bot.1 <| compl_inter_self t ▸ this
have : 𝓝[tᶜ] x ≠ ⊥ := hfx.of_inf_right.ne
absurd A this
