English
A set is closed iff every point outside has a neighborhood disjoint from the set, witnessed by the realizations.
Русский
Множество замкнуто тогда, когда у каждой точки вне множества есть окрестность, не пересекающая множество, свидетелем которой служат реализаторы.
LaTeX
$$$IsClosed(s) \\iff \\forall a, (\\forall b, a \\in F.F b \\rightarrow \\exists z \\in F.F b \\cap s, \n z \\notin s) \\rightarrow a \\in s$$$
Lean4
theorem isClosed_iff [TopologicalSpace α] (F : Realizer α) {s : Set α} :
IsClosed s ↔ ∀ a, (∀ b, a ∈ F.F b → ∃ z, z ∈ F.F b ∩ s) → a ∈ s :=
isOpen_compl_iff.symm.trans <|
F.isOpen_iff.trans <|
forall_congr' fun a ↦
show (a ∉ s → ∃ b : F.σ, a ∈ F.F b ∧ ∀ z ∈ F.F b, z ∉ s) ↔ _
by
haveI := Classical.propDecidable; rw [not_imp_comm]
simp [not_exists, not_and, not_forall, and_comm]
