proposition: Lemma PreFilterIntersection_glb {X : UU} (FF : PreFilter X → hProp) : (∏ F : PreFilter X, FF F → filter_le F (PreFilterIntersection FF)) × (∏ F : PreFilter X, (∏ G : PreFilter X, FF G → filter_le G F) → filter_le (PreFilterIntersection FF) F).
proof: Proof. split. - intros F Hf A Ha. now simple refine (Ha _ _). - intros F H A Fa G Hg. apply (H G Hg). apply Fa. Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA