class PiBase.RadialSpace (X : Type u) [TopologicalSpace X] : Prop

• ex_seq (A : Set X) (x : X) : x ∈ closure A → ∃ (s : Ordinal.{u}) (f : ↑(Set.Iio s) → X), 0 < s ∧ Set.range f ⊆ A ∧ Filter.Tendsto f Filter.atTop (nhds x)