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

• tendsto_constant (s : ℕ → X) (x : X) : Filter.Tendsto s Filter.atTop (nhds x) → ∀ᶠ (n : ℕ) in Filter.atTop, s n = x