proposition: Lemma continuous_subspace_in {U : topologicalType} (f : subspace A -> U) : continuous f = {in A, continuous f}.
proof: Proof. rewrite propeqE in_setP subspace_continuousP /continuous_at //=; split. by move=> Q x Ax; case: (nbhs_subspaceP x) => //=; exact: Q. by move=> + x Ax => /(_ x Ax); case: (nbhs_subspaceP x) => //=; exact: Q. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed