fact: Definition FilterDom {X : UU} (F : Filter X) (dom : X → hProp) (Hdom : ∏ P, F P → ∃ x, dom x ∧ P x) : Filter X.
imports: UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics UniMath.Topology.Prelim UniMath.MoreFoundations.PartA