class PiBase.α4Space (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).Nonempty}.Infinite