Theorems · Definition · general topology
IsSeqCompact
{X : Type u_1} → [TopologicalSpace X] → Set X → PropA set s is sequentially compact if every sequence taking values in s has a
converging subsequence.
- Defined in
- Mathlib.Topology.Defs.Sequences
- Cited by
- 26 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.
Cites6
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
- StrictMonoproof · cited by 706
Cited by28
Results whose statement or proof uses this declaration.
- IsCompact.isSeqCompactstatement · cited by 6
- IsSeqCompact.subseq_of_frequently_instatement and proof · cited by 5
- SeqCompactSpace.isSeqCompact_univstatement · cited by 3
- WeakDual.isSeqCompact_of_isBounded_of_isClosedstatement and proof · cited by 2
- IsSeqCompact.exists_tendstostatement and proof · cited by 1
- IsSeqCompact.exists_tendsto_of_frequently_memstatement and proof · cited by 1
- IsSeqCompact.imagestatement and proof · cited by 1
- IsSeqCompact.isCompactstatement and proof · cited by 1
- IsSeqCompact.isCompletestatement and proof · cited by 1
- IsSeqCompact.isCountablyCompactstatement and proof · cited by 1
- IsSeqCompact.rangestatement and proof · cited by 1
- IsSeqCompact.totallyBoundedstatement and proof · cited by 1