proposition: Lemma cvg_sigL (A : set U) (f : U -> V) (F : set_system (U -> V)) : Filter F -> {uniform A, F --> f} <-> {uniform, sigL A @ F --> sigL A f}.
proof: Proof. move=> FF; split. - move=> cvgF P' /uniform_nbhs [E [entE EsubP]]. apply: (filterS EsubP); apply: cvgF => /=. apply: (filterS (P := [set h | forall y, A y -> E(f y, h y)])). + by move=> h/= Eh [y ?] _; apply Eh; rewrite -inE. + by (apply/uniform_nbhs; eexists; split; eauto). - move=> cvgF P' /= /uniform_nbhs [ E [/= entE EsubP]]. apply: (filterS EsubP). move: (cvgF [set h | (forall y , E (sigL A f y, h y))]) => /=. set Q := (x in (_ -> x) -> _); move=> W. have: Q by apply W, uniform_nbhs; exists E; split => // h + ?; apply. rewrite {}/W {}/Q; near_simpl => /= R; apply: (filterS _ R) => h /=. by rewrite forall_sig /sigL /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed