proposition: Lemma uniform_limit_continuous_subspace {U : topologicalType} {V : uniformType} (K : set U) (F : set_system (U -> V)) (f : subspace K -> V) : ProperFilter F -> (\forall g \near F, continuous (g : subspace K -> V)) -> {uniform K, F --> f} -> {within K, continuous f}.
proof: Proof. move=> PF ctsF Ff; apply: (@subspace_eq_continuous _ _ _ (restrict K f)). by rewrite /restrict => ? ->. apply: (@uniform_limit_continuous (subspace K) _ (restrict K @ F) _). apply: (filterS _ ctsF) => g; apply: subspace_eq_continuous. by rewrite /restrict => ? ->. by apply (@uniform_restrict_cvg _ _ F ) => //; exact: PF. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed