proposition: Lemma uniform_restrict_cvg (F : set_system (U -> V)) (f : U -> V) A : Filter F -> {uniform A, F --> f} <-> {uniform, restrict A @ F --> restrict A f}.
proof: Proof. move=> FF; rewrite cvg_sigL; split. - rewrite -sigLK; move/(cvg_app valL) => D. apply: cvg_trans; first exact: D. move=> P /uniform_nbhs [E [/=entE EsubP]]; apply: (filterS EsubP). apply/uniform_nbhs; exists E; split=> //= h /=. rewrite /sigL => R u _; rewrite oinv_set_val. by case: insubP=> /= *; [apply: R|apply: entourage_refl]. - move/(@cvg_app _ _ _ _ (sigL A)). rewrite -fmap_comp sigL_restrict => D. apply: cvg_trans; first exact: D. move=> P /uniform_nbhs [E [/=entE EsubP]]; apply: (filterS EsubP). apply/uniform_nbhs; exists E; split=> //= h /=. rewrite /sigL => R [u Au] _ /=. by have := R u I; rewrite /patch Au. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed