proposition: Lemma interiorI (A B:set T): (A `&` B)^° = A^° `&` B^°.
proof: Proof. rewrite /interior predeqE => //= x; rewrite nbhsE; split => [[B0 ?] | []]. - by rewrite subsetI => // -[? ?]; split; exists B0. - by move=> -[B0 ? ?] [B1 ? ?]; exists (B0 `&` B1); [exact: open_nbhsI | rewrite subsetI; split; apply: subIset; [left|right]]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed