proposition: Lemma continuous_subspaceT_for {U} A (f : T -> U) (x : T) : A x -> {for x, continuous f} -> {for x, continuous (f : subspace A -> U)}.
proof: Proof. rewrite /continuous_at /prop_for => inA ctsf. have [_|//] := nbhs_subspaceP A x. apply: (cvg_trans _ ctsf); apply: cvg_fmap2; apply: cvg_within. exact: (nbhs_filter x). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed