proposition: Lemma closed_setIS (U : set (subspace A)) : closed A -> closed (U `&` A : set T) = closed U.
proof: Proof. move=> oA; apply/propext; rewrite closed_subspaceP. split=> [|[V [oV <-]]]; last exact: closedI. by move=> oUA; exists (U `&` A); rewrite -setIA setIid. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed