English
Let X be a topological space and s ⊆ X. Then s is closed if and only if for every x ∈ X and every filter F on X with F ≠ ⊥, if F ≤ 𝓟(s) and F ≤ 𝓝(x), then x ∈ s.
Русский
Пусть X — топологическое пространство и s ⊆ X. Тогда s замкнуто тогда и только тогда, когда для каждого x ∈ X и любого фильтра F на X, если F не нулевой и F ⊆ 𝓟(s) и F ⊆ 𝓝(x), то x ∈ s.
LaTeX
$$$ IsClosed\\,s \\iff \\forall x, \\forall F : Filter X, F.NeBot \\to F \\le 𝓟 s \\to F \\le 𝓝 x \\to x \\in s $$$
Lean4
theorem isClosed_iff_forall_filter : IsClosed s ↔ ∀ x, ∀ F : Filter X, F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s :=
by
simp_rw [isClosed_iff_clusterPt]
exact
⟨fun hs x F F_ne FS Fx ↦ hs _ <| NeBot.mono F_ne (le_inf Fx FS), fun hs x hx ↦
hs x (𝓝 x ⊓ 𝓟 s) hx inf_le_right inf_le_left⟩
