Theorems · Theorem · general topology
IsSeqClosed.isClosed
∀ {X : Type u_1} [inst : TopologicalSpace X] [SequentialSpace X] {s : Set X}, IsSeqClosed s → IsClosed sIn a sequential space, a sequentially closed set is closed.
- Defined in
- Mathlib.Topology.Defs.Sequences
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext, Quot.sound
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
- IsClosedstatement · cited by 1,639
- SequentialSpacestatement and proof · cited by 15
- IsSeqClosedstatement and proof · cited by 10
- SequentialSpace.isClosed_of_seqproof · cited by 1
Cited by9
Results whose statement or proof uses this declaration.
- IsClosed.upperClosure_piproof · cited by 2
- SeqContinuous.continuousproof · cited by 2
- IsClosed.lowerClosure_piproof · cited by 2
- SequentialSpace.coinducedproof · cited by 1
- SequentialSpace.iSupproof · cited by 1
- isClosed_iUnion_closure_singleton_of_not_tendstoproof · cited by 1
- LinearMap.continuous_of_seq_closed_graphproof · cited by 1
- isSeqClosed_iff_isClosedproof · cited by 0
- Topology.IsCoherentWith.of_seqproof · cited by 0