isSeqClosed_of_seqClosure_eq — Mathlib

English

If seqClosure s equals s, then s is sequentially closed.

Русский

Если seqClosure(s) = s, то s последовательностильно замкнуто.

LaTeX

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

Lean4

/-- If a set is equal to its sequential closure, then it is sequentially closed. -/
theorem isSeqClosed_of_seqClosure_eq {s : Set X} (hs : seqClosure s = s) : IsSeqClosed s := fun x _p hxs hxp =>
  hs ▸ ⟨x, hxs, hxp⟩

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