Sequences

📁 Source: Mathlib/Topology/Defs/Sequences.lean

Statistics

Metric	Count
Definitions FrechetUrysohnSpace, IsSeqClosed, IsSeqCompact, SeqCompactSpace, SeqContinuous, SequentialSpace, seqClosure	7
Theorems closure_subset_seqClosure, isClosed, isSeqCompact_univ, isClosed_of_seq, seqCompactSpace_iff	5
Total	12

FrechetUrysohnSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_subset_seqClosure 📖	mathematical	—	Set Set.instHasSubset closure seqClosure	—	—

IsSeqClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed 📖	mathematical	IsSeqClosed	IsClosed	—	SequentialSpace.isClosed_of_seq

SeqCompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeqCompact_univ 📖	mathematical	—	IsSeqCompact Set.univ	—	—

SequentialSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed_of_seq 📖	mathematical	IsSeqClosed	IsClosed	—	—

(root)

Definitions

Name	Category	Theorems
FrechetUrysohnSpace 📖	CompData	4 math math: Subtype.instFrechetUrysohnSpace, Topology.IsInducing.frechetUrysohnSpace, FirstCountableTopology.frechetUrysohnSpace, FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto
IsSeqClosed 📖	MathDef	5 math math: IsClosed.isSeqClosed, isSeqClosed_iff_isClosed, isSeqClosed_of_seqClosure_eq, isSeqClosed_iff, IsSeqClosed.preimage
IsSeqCompact 📖	MathDef	12 math math: SeqCompactSpace.isSeqCompact_univ, IsCountablyCompact.isSeqCompact, UniformSpace.isCompact_iff_isSeqCompact, WeakDual.isSeqCompact_closedBall, isCompact_iff_isSeqCompact, isCountablyCompact_iff_isSeqCompact, WeakDual.isSeqCompact_of_isBounded_of_isClosed, IsSeqCompact.image, WeakDual.isSeqCompact_polar, seqCompactSpace_iff, IsCompact.isSeqCompact, IsSeqCompact.range
SeqCompactSpace 📖	CompData	5 math math: UniformSpace.compactSpace_iff_seqCompactSpace, FirstCountableTopology.seq_compact_of_compact, compactSpace_iff_seqCompactSpace, seqCompactSpace_iff, CountablyCompactSpace.SeqCompactSpace
SeqContinuous 📖	MathDef	2 math math: Continuous.seqContinuous, continuous_iff_seqContinuous
SequentialSpace 📖	CompData	12 math math: FrechetUrysohnSpace.to_sequentialSpace, Quotient.instSequentialSpace, Topology.IsQuotientMap.sequentialSpace, DeltaGeneratedSpace.instSequentialSpace, SequentialSpace.iSup, LightCondSet.instSequentialSpaceCarrierObjTopCatLightCondSetToTopCat, Sum.instSequentialSpace, Sigma.instSequentialSpace, LightCondSet.instSequentialSpaceCarrierToTopCat, Sequential.is_sequential, SequentialSpace.sup, SequentialSpace.coinduced
seqClosure 📖	CompOp	6 math math: IsSeqClosed.seqClosure_eq, seqClosure_eq_closure, subset_seqClosure, isSeqClosed_iff, seqClosure_subset_closure, FrechetUrysohnSpace.closure_subset_seqClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
seqCompactSpace_iff 📖	mathematical	—	SeqCompactSpace IsSeqCompact Set.univ	—	—

---

← Back to Index