proposition: Lemma meets_globallyr T F (B : set T) : F `#` globally B = forall A, F A -> A `&` B !=set0.
proof: Proof. by rewrite meetsC meets_globallyl; under eq_forall do rewrite setIC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed