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. split. - intros F Hf A Ha. now simple refine (Ha _ _). - intros F H A Fa G Hg. apply (H G Hg). apply Fa. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.