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