theorem Filter.iSup_liminf_le_liminf_iSup {α : Type u_1} {β : Type u_2} {ι : Sort u_3} [CompleteLattice α] {f : Filter β} {u : ι → β → α} : ⨆ (i : ι), liminf (u i) f ≤ liminf (fun (b : β) => ⨆ (i : ι), u i b) f