proposition: Lemma open_subspaceIT (U : set (subspace A)) : open (U `&` A) = open U.
proof: Proof. apply/propext; split; last first. by move=> oU; apply: openI => //; apply: open_subspaceT. move=> oUA; rewrite (_ : U = (U `&` A) `|` (U `&` ~`A)). by apply: openU => //; apply: open_subspace_out => ? []. by rewrite -setIUr setUCr setIT. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed