proposition: Lemma subspace_continuousP {S : topologicalType} (f : T -> S) : continuous (f : subspace A -> S) <-> (forall x, A x -> f @ within A (nbhs x) --> f x) .
proof: Proof. split => [ctsf x Ax W /=|wA x]. by rewrite nbhs_simpl //= nbhs_subspace_in //=; apply: ctsf. rewrite /continuous_at; case: _ / (nbhs_subspaceP x) => Ax. exact: (cvg_trans _ (wA _ Ax)). by move=> ? /nbhs_singleton //= ?; rewrite nbhs_simpl => ? ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed