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

• subset_converge {x : X} {S : ℕ → ℕ → X} (S_inj : ∀ (n : ℕ), Function.Injective (S n)) (S_disj : Pairwise fun (n m : ℕ) => Set.range (S n) ∩ Set.range (S m) = ∅) (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}.Infinite