proposition: Lemma closureI (A B : set T) : closure (A `&` B) `<=` closure A `&` closure B.
proof: Proof. by move=> p clABp; split=> ? /clABp [q [[]]]; exists q. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed