Lemma filterlim_incr_2 {X Y : UU} : ∏ (f : X → Y) (F : PreFilter X) (G G' : PreFilter Y), filter_le G G' → filterlim f F G → filterlim f F G'. Proof. intros f F G G' Hg Hle A Ha. specialize (Hg _ Ha). specialize (Hle _ Hg). exact Hle. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.