proposition: Lemma wopI (A B : set W) : wopen A -> wopen B -> wopen (A `&` B).
proof: Proof. by move=> [C Cop <-] [D Dop <-]; exists (C `&` D) => //; apply: openI. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed