English
In a Frechet-Urysohn space, a point a belongs to the closure of a set s if and only if there exists a sequence x_n in s converging to a.
Русский
В пространстве Фреше–Ури́шхо́н точка a принадлежит замыканию множества s тогда и только тогда существует последовательность x_n из s, сходящаяся к a.
LaTeX
$$$a \in \overline{s} \iff \exists x: \mathbb{N} \to X, (\forall n, x(n) \in s) \land \operatorname{Tendsto}(x)\,\text{atTop}\,(\mathcal{N}(a))$$$
Lean4
/-- In a Fréchet-Urysohn space, a point belongs to the closure of a set iff it is a limit
of a sequence taking values in this set. -/
theorem mem_closure_iff_seq_limit [FrechetUrysohnSpace X] {s : Set X} {a : X} :
a ∈ closure s ↔ ∃ x : ℕ → X, (∀ n : ℕ, x n ∈ s) ∧ Tendsto x atTop (𝓝 a) :=
by
rw [← seqClosure_eq_closure]
rfl
