proposition: Lemma subspace_eq_continuous {S : topologicalType} (f g : subspace A -> S) : {in A, f =1 g} -> continuous f -> continuous g.
proof: Proof. rewrite ?subspace_continuousP => feq L x Ax; rewrite -(feq x) ?inE //. by apply: cvg_trans _ (L x Ax); apply: fmap_within_eq=> ? ?; rewrite feq. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed