Commit 2024-02-27 07:41 51d070d7

View on Github →

chore(Topology/Sequences): split file (#10943) I want to have access to the definitions much earlier. Also, most of the file doesn't need metric spaces at all.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Defs/Sequences.lean

added def IsSeqClosed

added def IsSeqCompact

added def SeqContinuous

added def seqClosure

Created Mathlib/Topology/MetricSpace/Sequences.lean

added theorem tendsto_subseq_of_bounded

added theorem tendsto_subseq_of_frequently_bounded

Modified Mathlib/Topology/Sequences.lean

deleted def IsSeqClosed

deleted def IsSeqCompact

deleted def SeqContinuous

deleted def seqClosure

deleted theorem tendsto_subseq_of_bounded

deleted theorem tendsto_subseq_of_frequently_bounded