seqClosure_eq — Mathlib

English

In the namespace of sequential closed sets, seqClosure s equals s when s is sequentially closed.

Русский

В рамках понятия последовательной замкнутости, seqClosure s совпадает с s, когда s последовательнос замкнуто.

LaTeX

$$$ \mathrm{IsSeqClosed}(s) \Rightarrow \mathrm{seqClosure}(s) = s $$$

Lean4

/-- The sequential closure of a sequentially closed set is the set itself. -/
theorem seqClosure_eq {s : Set X} (hs : IsSeqClosed s) : seqClosure s = s :=
  Subset.antisymm (fun _p ⟨_x, hx, hp⟩ => hs hx hp) subset_seqClosure

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