proposition: Lemma cvg_switch_1 {U : uniformType} F1 {FF1 : ProperFilter F1} F2 {FF2 : Filter F2} (f : T1 -> T2 -> U) (g : T2 -> U) (h : T1 -> U) (l : U) : f @ F1 --> g -> (forall x1, f x1 @ F2 --> h x1) -> h @ F1 --> l -> g @ F2 --> l.
proof: Proof. move=> fg fh hl; apply/cvg_app_entourageP => A entA. near F1 => x1; near=> x2; apply: (entourage_split (h x1)) => //. by near: x1; apply/(hl (to_set _ l)) => /=. apply: (entourage_split (f x1 x2)) => //. by near: x2; apply/(fh x1 (to_set _ _)) => /=. move: (x2); near: x1; have /cvg_fct_entourageP /(_ (_^-1%classic)):= fg; apply. exact: entourage_inv. Unshelve. all: by end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed