proposition: Lemma cvg_uniformU (f : U -> V) (F : set_system (U -> V)) A B : Filter F -> {uniform A, F --> f} -> {uniform B, F --> f} -> {uniform (A `|` B), F --> f}.
proof: Proof. move=> FF AFf BFf Q /=/uniform_nbhs [E [entE EsubQ]]. apply: (filterS EsubQ). rewrite (_: [set h | (forall y : U, (A `|` B) y -> E (f y, h y))] = [set h | forall y, A y -> E (f y, h y)] `&` [set h | forall y, B y -> E (f y, h y)]). - apply: filterI; [apply: AFf| apply: BFf]. + by apply/uniform_nbhs; exists E; split. + by apply/uniform_nbhs; exists E; split. - rewrite eqEsubset; split=> h. + by move=> R; split=> t ?; apply: R;[left| right]. + by move=> [R1 R2] y [? | ?]; [apply: R1| apply: R2]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed