Sequences

📁 Source: Mathlib/Topology/Sequences.lean

Statistics

Metric	Count
Definitions	0
Theorems tendsto_subseq, seqContinuous, frechetUrysohnSpace, seq_compact_of_compact, of_seq_tendsto_imp_tendsto, to_sequentialSpace, isSeqClosed, isSeqCompact, tendsto_subseq, tendsto_subseq', preimage, seqClosure_eq, exists_tendsto, exists_tendsto_of_frequently_mem, image, isCompact, isComplete, range, subseq_of_frequently_in, totallyBounded, instSequentialSpace, tendsto_subseq, continuous, coinduced, iSup, sup, instSequentialSpace, instFrechetUrysohnSpace, instSequentialSpace, frechetUrysohnSpace, sequentialSpace, compactSpace_iff_seqCompactSpace, isCompact_iff_isSeqCompact, compactSpace_iff_seqCompactSpace, continuous_iff_seqContinuous, isCompact_iff_isSeqCompact, isSeqClosed_iff, isSeqClosed_iff_isClosed, isSeqClosed_of_seqClosure_eq, mem_closure_iff_seq_limit, seqClosure_eq_closure, seqClosure_subset_closure, subset_seqClosure, tendsto_nhds_iff_seq_tendsto	44
Total	44

CompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_subseq 📖	mathematical	—	StrictMono Nat.instPreorder Filter.Tendsto Filter.atTop nhds	—	SeqCompactSpace.tendsto_subseq FirstCountableTopology.seq_compact_of_compact

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
seqContinuous 📖	mathematical	Continuous	SeqContinuous	—	Filter.Tendsto.comp tendsto

FirstCountableTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
frechetUrysohnSpace 📖	mathematical	—	FrechetUrysohnSpace	—	FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto Filter.tendsto_iff_seq_tendsto nhds_generated_countable
seq_compact_of_compact 📖	mathematical	—	SeqCompactSpace	—	IsCompact.isSeqCompact isCompact_univ

FrechetUrysohnSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_seq_tendsto_imp_tendsto 📖	mathematical	ContinuousAt sierpinskiSpace	FrechetUrysohnSpace	—	subset_seqClosure Filter.extraction_of_frequently_atTop Filter.Tendsto.comp StrictMono.tendsto_atTop
to_sequentialSpace 📖	mathematical	—	SequentialSpace	—	closure_eq_iff_isClosed seqClosure_eq_closure IsSeqClosed.seqClosure_eq

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeqClosed 📖	mathematical	—	IsSeqClosed	—	mem_of_tendsto Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Filter.Eventually.of_forall

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeqCompact 📖	mathematical	IsCompact	IsSeqCompact	—	Filter.map_neBot Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Filter.tendsto_principal Filter.Eventually.of_forall TopologicalSpace.FirstCountableTopology.tendsto_subseq
tendsto_subseq 📖	mathematical	IsCompact Set Set.instMembership	StrictMono Nat.instPreorder Filter.Tendsto Filter.atTop nhds	—	isSeqCompact
tendsto_subseq' 📖	mathematical	IsCompact Filter.Frequently Set Set.instMembership Filter.atTop Nat.instPreorder	StrictMono Filter.Tendsto nhds	—	IsSeqCompact.subseq_of_frequently_in isSeqCompact

IsSeqClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preimage 📖	mathematical	IsSeqClosed SeqContinuous	Set.preimage	—	—
seqClosure_eq 📖	mathematical	IsSeqClosed	seqClosure	—	Set.Subset.antisymm subset_seqClosure

IsSeqCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_tendsto 📖	mathematical	IsSeqCompact UniformSpace.toTopologicalSpace Set Set.instMembership CauchySeq Nat.instPreorder	Filter.Tendsto Filter.atTop nhds	—	exists_tendsto_of_frequently_mem Filter.Frequently.of_forall Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder
exists_tendsto_of_frequently_mem 📖	mathematical	IsSeqCompact UniformSpace.toTopologicalSpace Filter.Frequently Set Set.instMembership Filter.atTop Nat.instPreorder CauchySeq	Filter.Tendsto nhds	—	subseq_of_frequently_in tendsto_nhds_of_cauchySeq_of_subseq Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder StrictMono.tendsto_atTop
image 📖	mathematical	SeqContinuous IsSeqCompact	Set.image	—	Set.mem_image_of_mem Filter.Tendsto.congr
isCompact 📖	mathematical	IsSeqCompact	IsCompact	—	isCompact_iff_totallyBounded_isComplete totallyBounded isComplete TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated
isComplete 📖	mathematical	IsSeqCompact UniformSpace.toTopologicalSpace	IsComplete	—	Filter.exists_antitone_basis refl_mem_uniformity Filter.inter_mem Filter.prod_mem_prod Filter.le_principal_iff Filter.HasBasis.mem_iff Filter.HasBasis.prod_self Filter.basis_sets Set.iInter₂_subset le_refl Set.biInter_subset_biInter_left LE.le.trans Filter.biInter_mem Set.finite_le_nat HasSubset.Subset.trans Set.instIsTransSubset Set.prod_mono Filter.HasBasis.cauchySeq_iff Filter.HasAntitoneBasis.toHasBasis exists_tendsto Filter.HasBasis.ge_iff nhds_basis_uniformity' Filter.Eventually.exists Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Filter.Eventually.and Filter.eventually_ge_atTop UniformSpace.ball_mem_nhds Filter.mem_of_superset Filter.nonempty_of_mem comp_mem_uniformity_sets Filter.HasAntitoneBasis.mem
range 📖	mathematical	SeqContinuous	IsSeqCompact Set.range	—	Set.image_univ image SeqCompactSpace.isSeqCompact_univ
subseq_of_frequently_in 📖	mathematical	IsSeqCompact Filter.Frequently Set Set.instMembership Filter.atTop Nat.instPreorder	StrictMono Filter.Tendsto nhds	—	Filter.extraction_of_frequently_atTop StrictMono.comp
totallyBounded 📖	mathematical	IsSeqCompact UniformSpace.toTopologicalSpace	TotallyBounded	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq Mathlib.Tactic.Push.not_forall_eq Set.seq_of_forall_finite_exists CauchySeq.mem_entourage Filter.Tendsto.cauchySeq le_rfl

Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSequentialSpace 📖	mathematical	—	SequentialSpace instTopologicalSpaceQuotient	—	Topology.IsQuotientMap.sequentialSpace

SeqCompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_subseq 📖	mathematical	—	StrictMono Nat.instPreorder Filter.Tendsto Filter.atTop nhds	—	isSeqCompact_univ Set.mem_univ

SeqContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous 📖	mathematical	SeqContinuous	Continuous	—	continuous_iff_isClosed IsSeqClosed.isClosed IsSeqClosed.preimage IsClosed.isSeqClosed

SequentialSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coinduced 📖	mathematical	—	SequentialSpace TopologicalSpace.coinduced	—	isClosed_coinduced IsSeqClosed.isClosed IsSeqClosed.preimage Continuous.seqContinuous continuous_coinduced_rng
iSup 📖	mathematical	SequentialSpace	iSup TopologicalSpace ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	isClosed_iSup_iff IsSeqClosed.isClosed Filter.Tendsto.mono_right nhds_mono le_iSup
sup 📖	mathematical	—	SequentialSpace TopologicalSpace SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	sup_eq_iSup iSup

Sigma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSequentialSpace 📖	mathematical	SequentialSpace	instTopologicalSpaceSigma	—	SequentialSpace.iSup SequentialSpace.coinduced

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFrechetUrysohnSpace 📖	mathematical	—	FrechetUrysohnSpace instTopologicalSpaceSubtype	—	Topology.IsInducing.frechetUrysohnSpace Topology.IsInducing.subtypeVal

Sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSequentialSpace 📖	mathematical	—	SequentialSpace instTopologicalSpaceSum	—	SequentialSpace.sup SequentialSpace.coinduced

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
frechetUrysohnSpace 📖	mathematical	Topology.IsInducing	FrechetUrysohnSpace	—	mem_closure_iff_seq_limit Set.mem_preimage closure_eq_preimage_closure_image tendsto_nhds_iff

Topology.IsQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sequentialSpace 📖	mathematical	Topology.IsQuotientMap	SequentialSpace	—	SequentialSpace.coinduced eq_coinduced

UniformSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace_iff_seqCompactSpace 📖	mathematical	—	CompactSpace SeqCompactSpace	—	compactSpace_iff_seqCompactSpace
isCompact_iff_isSeqCompact 📖	mathematical	—	IsCompact IsSeqCompact	—	isCompact_iff_isSeqCompact

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace_iff_seqCompactSpace 📖	mathematical	—	CompactSpace SeqCompactSpace	—	—
continuous_iff_seqContinuous 📖	mathematical	—	Continuous SeqContinuous	—	Continuous.seqContinuous SeqContinuous.continuous
isCompact_iff_isSeqCompact 📖	mathematical	—	IsCompact IsSeqCompact	—	IsCompact.isSeqCompact TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology IsSeqCompact.isCompact
isSeqClosed_iff 📖	mathematical	—	IsSeqClosed seqClosure	—	IsSeqClosed.seqClosure_eq isSeqClosed_of_seqClosure_eq
isSeqClosed_iff_isClosed 📖	mathematical	—	IsSeqClosed IsClosed	—	IsSeqClosed.isClosed IsClosed.isSeqClosed
isSeqClosed_of_seqClosure_eq 📖	mathematical	seqClosure	IsSeqClosed	—	—
mem_closure_iff_seq_limit 📖	mathematical	—	Set Set.instMembership closure Filter.Tendsto Filter.atTop Nat.instPreorder nhds	—	seqClosure_eq_closure
seqClosure_eq_closure 📖	mathematical	—	seqClosure closure	—	HasSubset.Subset.antisymm Set.instAntisymmSubset seqClosure_subset_closure FrechetUrysohnSpace.closure_subset_seqClosure
seqClosure_subset_closure 📖	mathematical	—	Set Set.instHasSubset seqClosure closure	—	mem_closure_of_tendsto Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Filter.univ_mem'
subset_seqClosure 📖	mathematical	—	Set Set.instHasSubset seqClosure	—	tendsto_const_nhds
tendsto_nhds_iff_seq_tendsto 📖	mathematical	—	Filter.Tendsto nhds Filter.atTop Nat.instPreorder	—	Filter.Tendsto.comp Filter.HasBasis.tendsto_iff nhds_basis_closeds seqClosure_eq_closure IsClosed.mem_of_tendsto Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Filter.Eventually.of_forall isClosed_closure subset_closure

---

← Back to Index