English
A closed neighborhood relation: if s is compact, f ≤ 𝓟 s, t is open, and every x ∈ s which is a ClusterPt of f lies in t, then t ∈ f.
Русский
Если s компактно, f ≤ 𝓟 s, t открыто, и каждый x ∈ s, являющийся ClusterPt для f, принадлежит t, то t ∈ f.
LaTeX
$$$IsCompact(s) \rightarrow (f \le 𝓟 s) \rightarrow IsOpen(t) \rightarrow (\forall x \in s, ClusterPt x f \rightarrow x \in t) \rightarrow t \in f$$$
Lean4
theorem adherence_nhdset {f : Filter X} (hs : IsCompact s) (hf₂ : f ≤ 𝓟 s) (ht₁ : IsOpen t)
(ht₂ : ∀ x ∈ s, ClusterPt x f → x ∈ t) : t ∈ f :=
Classical.by_cases mem_of_eq_bot fun (this : f ⊓ 𝓟 tᶜ ≠ ⊥) =>
let ⟨x, hx, (hfx : ClusterPt x <| f ⊓ 𝓟 tᶜ)⟩ := @hs _ ⟨this⟩ <| inf_le_of_left_le hf₂
have : x ∈ t := ht₂ x hx hfx.of_inf_left
have : tᶜ ∩ t ∈ 𝓝[tᶜ] x := inter_mem_nhdsWithin _ (IsOpen.mem_nhds ht₁ 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
