class PiBase.UsSpace (X : Type u_1) [TopologicalSpace X] : Prop

• us (f : ℕ → X) (a b : X) : Filter.Tendsto f Filter.atTop (nhds a) → Filter.Tendsto f Filter.atTop (nhds b) → a = b