∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α}
  [inst_1 : CompleteLattice γ] (g : sSupHom α γ), g (Filter.blimsup u f p) ≤ Filter.blimsup (⇑g ∘ u) f p