Lemma FilterIm_incr {X Y : UU} : ∏ (f : X → Y) (F G : Filter X), filter_le F G → filter_le (FilterIm f F) (FilterIm f G). Proof. intros f F G Hle A ; simpl. apply Hle. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.