class PiBase.α1Space (X : Type u_1) [TopologicalSpace X] : Prop

• subset_converge {x : X} {S : ℕ → ℕ → X} (S_inj : ∀ (n : ℕ), Function.Injective (S n)) (hS : ∀ (n : ℕ), Filter.Tendsto (S n) Filter.atTop (nhds x)) : ∃ (T : ℕ → X), Function.Injective T ∧ Filter.Tendsto T Filter.atTop (nhds x) ∧ Set.range T ⊆ ⋃ (n : ℕ), Set.range (S n) ∧ ∀ (n : ℕ), (Set.range (S n) \ Set.range T).Finite