∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
  [OrderTopology R] (F : Filter ι) [inst_3 : AddCommSemigroup R] [inst_4 : Sub R] [ContinuousSub R] [OrderedSub R]
  [AddLeftMono R] (f : ι → R) (c : R),
  Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) F f →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) F f → Filter.limsup (fun i => c - f i) F = c - Filter.liminf f F