proposition: Lemma PreFilterBase_le {X : UU} (base base' : BaseOfPreFilter X) : (∏ P : X → hProp, base P → ∃ Q : X → hProp, base' Q × (∏ x, Q x → P x)) <-> filter_le (PreFilterBase base') (PreFilterBase base).
proof: Proof. split. - intros Hbase P. apply (pr1 (filterbase_le base base')), Hbase. - apply (pr2 (filterbase_le base base')). Qed.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA