proposition: Lemma continuous_subspace0 {U} (f : T -> U) : {within set0, continuous f}.
proof: Proof. move=> x Q /=. by case: (nbhs_subspaceP (@set0 T) x) => // _ /nbhs_singleton /= ? ? ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed