proposition: Lemma subspaceT_continuous {U} A (B : set U) (f : {fun A >-> B}) : {within A, continuous f} -> continuous (f : subspace A -> subspace B).
proof: Proof. move=> /continuousP ctsf; apply/continuousP => O /open_subspaceP [V [oV VBOB]]. rewrite -open_subspaceIT; apply/open_subspaceP. case/open_subspaceP: (ctsf _ oV) => W [oW fVA]; exists W; split => //. rewrite fVA -setIA setIid eqEsubset; split => x [fVx Ax]; split => //. - by have /[!VBOB]-[] : (V `&` B) (f x) by split => //; exact: funS. - by have /[!esym VBOB]-[] : (O `&` B) (f x) by split => //; exact: funS. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed