Definition filterlim {X Y : UU} (f : X → Y) (F : PreFilter X) (G : PreFilter Y) := filter_le (PreFilterIm f F) G.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.