proposition: Lemma continuous_open_subspace {U} A (f : T -> U) : open A -> {within A, continuous f} = {in A, continuous f}.
proof: Proof. rewrite openE continuous_subspace_in /= => oA; rewrite propeqE ?in_setP. by split => + x /[dup] Ax /oA Aox => /(_ _ Ax); rewrite /continuous_at -(nbhs_subspace_interior Aox). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed