Theorem tendsto_subseq_of_bounded

Modification history

2024-02-27 07:41

Mathlib/Topology/MetricSpace/Sequences.lean

chore(Topology/Sequences): split file (#10943) …

Modified tendsto_subseq_of_bounded View on Github →

2023-09-19 04:03

Mathlib/Topology/Sequences.lean

refactor(Topology/MetricSpace): remove `Metric.Bounded` (#7240) …

Modified tendsto_subseq_of_bounded View on Github →

2023-03-03 21:38

Mathlib/Topology/Sequences.lean

feat: port Topology.Sequences (#2604)

Added tendsto_subseq_of_bounded View on Github →