proposition: Lemma FilterIntersection_glb {X : UU} (FF : Filter X → hProp) Hff : (∏ F : Filter X, FF F → filter_le F (FilterIntersection FF Hff)) × (∏ F : Filter X, (∏ G : Filter X, FF G → filter_le G F) → filter_le (FilterIntersection FF Hff) 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