proposition: Lemma PreFilterIm_incr {X Y : UU} : ∏ (f : X → Y) (F G : PreFilter X), filter_le F G → filter_le (PreFilterIm f F) (PreFilterIm f G).
proof: Proof. intros f F G Hle A ; simpl. apply Hle. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA