∀ {R : Type u_5} {S : Type u_6} {F : Filter R} [inst : LinearOrder R] [inst_1 : LinearOrder S] {f : R → S},
  Antitone f →
    ∀ [F.NeBot], Filter.IsCobounded (fun x1 x2 => x1 ≥ x2) F → Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f