∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [FirstCountableTopology α]
  [OrderTopology α] {f : Filter β} [CountableInterFilter f] {u : β → α}, (Filter.limsup u f = ⊥) = (u =ᶠ[f] ⊥)