∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [Nonempty β] [inst_2 : SemilatticeSup β] {u : β → α} {a : α},
  Filter.Tendsto u Filter.atTop (nhds a) = ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε