proposition: Lemma continuous_subspace1 {U} (a : T) (f : T -> U) : {within [set a], continuous f}.
proof: Proof. move=> x Q /=. case: (nbhs_subspaceP [set a] x); last by move=> _ /nbhs_singleton /= ? ? ->. by move=> -> /nbhs_singleton ?; apply: nearW => ? ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed