proposition: 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: Proof. intros f F F' G Hf Hle A Ha. specialize (Hle _ Ha). specialize (Hf _ Hle). apply Hf. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA