seqClosure_eq_closure — Mathlib

English

In Frechet-Urysohn spaces, the sequential closure of a set equals its topological closure.

Русский

Во пространствах Фреше–Ури́схо́н последовательное замыкание множества совпадает с его топологическим замыканием.

LaTeX

$$$\operatorname{seqClosure}(s) = \operatorname{closure}(s)$$$

Lean4

theorem seqClosure_eq_closure [FrechetUrysohnSpace X] (s : Set X) : seqClosure s = closure s :=
  seqClosure_subset_closure.antisymm <| FrechetUrysohnSpace.closure_subset_seqClosure s

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