Theorems · Definition · general topology
IsSeqClosed
{X : Type u_1} → [TopologicalSpace X] → Set X → PropA set s is sequentially closed if for any converging sequence x n of elements of s, the
limit belongs to s as well. Note that the sequential closure of a set is not guaranteed to be
sequentially closed.
- Defined in
- Mathlib.Topology.Defs.Sequences
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- nhdsproof · cited by 5,554
- Filter.Tendstoproof · cited by 3,814
- Filter.atTopproof · cited by 2,405
Cited by12
Results whose statement or proof uses this declaration.
- IsSeqClosed.isClosedstatement and proof · cited by 9
- IsSeqClosed.preimagestatement and proof · cited by 2
- IsClosed.isSeqClosedstatement · cited by 2
- SequentialSpace.coinducedproof · cited by 1
- isSeqClosed_of_seqClosure_eqstatement · cited by 1
- IsSeqClosed.seqClosure_eqstatement and proof · cited by 1
- SequentialSpace.isClosed_of_seqstatement · cited by 1
- SequentialSpace.iSupproof · cited by 1
- SequentialSpace.casesOnstatement and proof · cited by 0
- isSeqClosed_iffstatement · cited by 0
- isSeqClosed_iff_isClosedstatement · cited by 0
- SequentialSpace.recOnstatement and proof · cited by 0