proposition: Lemma closure_subspaceW (U : set T) : U `<=` A -> closure (U : set (subspace A)) = closure (U : set T) `&` A.
proof: Proof. have /closed_subspaceP := (@closed_closure _ (U : set (subspace A))). move=> [V] [clV VAclUA]. move=> /[dup] /(@closure_subset [the topologicalType of subspace _]). have /closure_id <- := closed_subspaceT => /setIidr <-; rewrite setIC. move=> UsubA; rewrite eqEsubset; split. apply: setSI; rewrite closureE; apply: smallest_sub (@subset_closure _ U). by apply: closed_subspaceW; exact: closed_closure. rewrite -VAclUA; apply: setSI; rewrite closureE //=; apply: smallest_sub => //. apply: subset_trans (@subIsetl _ V A); rewrite VAclUA subsetI; split => //. exact: (@subset_closure _ (U : set (subspace A))). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed