proposition: Lemma continuous_subspaceT {U} A (f : T -> U) : continuous f -> {within A, continuous f}.
proof: Proof. move=> ctsf; rewrite continuous_subspace_in => ? ?. exact: continuous_in_subspaceT. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed