proposition: Lemma continuous_in_subspaceT {U} A (f : T -> U) : {in A, continuous f} -> {within A, continuous f}.
proof: Proof. rewrite continuous_subspace_in ?in_setP => ctsf t At. by apply: continuous_subspaceT_for => //=; apply: ctsf. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed