isClosed_iff_frequently — Mathlib

English

A set s is closed iff for every x, whenever there are frequently points y near x with y ∈ s, then x ∈ s.

Русский

Множество s замкнуто тогда и только тогда, когда для каждой точки x, если рядом с x часто встречаются точки y ∈ s, то x ∈ s.

LaTeX

$$$\\text{IsClosed}(s) \\iff \\forall x, (\\exists^\\mathrm{f} y \\in \\mathcal{N}(x), y \\in s) \\to x \\in s$$$

Lean4

/-- A set `s` is closed iff for every point `x`, if there is a point `y` close to `x` that belongs
to `s` then `x` is in `s`. -/
theorem isClosed_iff_frequently : IsClosed s ↔ ∀ x, (∃ᶠ y in 𝓝 x, y ∈ s) → x ∈ s :=
  by
  rw [← closure_subset_iff_isClosed]
  refine forall_congr' fun x => ?_
  rw [mem_closure_iff_frequently]

Похожие утверждения