proposition: Lemma filter_from_filter {I T : Type} (D : set I) (B : I -> set T) : (exists i : I, D i) -> (forall i j, D i -> D j -> exists2 k, D k & B k `<=` B i `&` B j) -> Filter (filter_from D B).
proof: Proof. move=> [i0 Di0] Binter; constructor; first by exists i0. move=> P Q [i Di BiP] [j Dj BjQ]; have [k Dk BkPQ]:= Binter _ _ Di Dj. by exists k => // x /BkPQ [/BiP ? /BjQ]. by move=> P Q subPQ [i Di BiP]; exists i => //; apply: subset_trans subPQ. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed