Theorem tendsto_subseq_of_frequently_bounded

Modification history

2024-02-27 07:41
Mathlib/Topology/MetricSpace/Sequences.lean
chore(Topology/Sequences): split file (#10943) …
Modified tendsto_subseq_of_frequently_boundedView on Github →
2023-09-19 04:03
Mathlib/Topology/Sequences.lean
refactor(Topology/MetricSpace): remove `Metric.Bounded` (#7240) …
Modified tendsto_subseq_of_frequently_boundedView on Github →
2023-03-03 21:38
Mathlib/Topology/Sequences.lean
feat: port Topology.Sequences (#2604)
Added tendsto_subseq_of_frequently_boundedView on Github →