English
A point x belongs to the closure of s if and only if every open neighborhood of x meets s.
Русский
Точка x принадлежит замыканию s тогда и только тогда, когда каждое открытое окрестности x встречает s.
LaTeX
$$$x \\\\in \\\\overline{s} \\\\iff \\\\forall o, IsOpen(o) \\\\to x \\\\in o \\\\to (o \\cap s).Nonempty$$$
Lean4
theorem mem_closure_iff : x ∈ closure s ↔ ∀ o, IsOpen o → x ∈ o → (o ∩ s).Nonempty :=
⟨fun h o oo ao =>
by_contradiction fun os =>
have : s ⊆ oᶜ := fun x xs xo => os ⟨x, xo, xs⟩
closure_minimal this (isClosed_compl_iff.2 oo) h ao,
fun H _ ⟨h₁, h₂⟩ =>
by_contradiction fun nc =>
let ⟨_, hc, hs⟩ := H _ h₁.isOpen_compl nc
hc (h₂ hs)⟩
