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