∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : LinearOrder β] {f : Filter α} {F : ι → α → β} {s : Finset ι}
  (hs : s.Nonempty),
  (∃ i ∈ s, Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (F i)) →
    Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f fun a => s.inf' hs fun i => F i a