Sequences

Statistics

Metric	Count
Definitions	0
Theorems `tendsto_subseq_of_bounded`, `tendsto_subseq_of_frequently_bounded`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_subseq_of_bounded` 📖	mathematical	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `Set` `Set.instMembership`	`closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `StrictMono` `Nat.instPreorder` `Filter.Tendsto` `Filter.atTop` `nhds`	—	`tendsto_subseq_of_frequently_bounded` `Filter.Frequently.of_forall` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat`
`tendsto_subseq_of_frequently_bounded` 📖	mathematical	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `Filter.Frequently` `Set` `Set.instMembership` `Filter.atTop` `Nat.instPreorder`	`closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `StrictMono` `Filter.Tendsto` `nhds`	—	`IsCompact.isSeqCompact` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `UniformSpace.pseudoMetrizableSpace` `EMetric.instIsCountablyGeneratedUniformity` `Bornology.IsBounded.isCompact_closure` `Filter.Frequently.mono` `subset_closure` `IsSeqCompact.subseq_of_frequently_in`

---