proposition: Lemma FilterBase_Generated_hypothesis {X : UU} (base : BaseOfFilter X) : ∏ L' : Sequence (X → hProp), (∏ m : stn (length L'), base (L' m)) → ∃ x : X, finite_intersection L' x.
proof: Proof. apply filterbase_generated_hypothesis. - intros A B. apply (BaseOfFilter_and base). - apply (BaseOfFilter_notempty base). - intros A Ha. now apply (BaseOfFilter_notfalse base). Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA