proposition: Lemma near_powerset_filter_fromP (P : set Y -> Prop) : (forall A B, A `<=` B -> P B -> P A) -> (\forall U \near powerset_filter_from, P U) <-> exists2 U, F U & P U.
proof: Proof. move=> Psub; split=> [[M [FM ? [U MU]]] MsubP|[U FU PU]]. by exists U; [exact: FM | exact: MsubP]. exists [set V | F V /\ V `<=` U]; last by move=> V [_] /Psub; exact. split=> [E [] //| |]; last by exists U; split. by move=> E1 E2 [F1 E1U F2 E2subE1]; split => //; exact: subset_trans E1U. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed