proposition: Lemma cvg_switch_2 {U : completeType} F1 {FF1 : ProperFilter F1} F2 {FF2 : ProperFilter F2} (f : T1 -> T2 -> U) (g : T2 -> U) (h : T1 -> U) : f @ F1 --> g -> (forall x, f x @ F2 --> h x) -> [cvg h @ F1 in U].
proof: Proof. move=> fg fh; apply: cauchy_cvg => A entA. rewrite !near_simpl -near2_pair near_map2; near=> x1 y1 => /=; near F2 => x2. apply: (entourage_split (f x1 x2)) => //. by near: x2; apply/(fh _ (to_set _ _)) => /=. apply: (entourage_split (f y1 x2)) => //; last first. near: x2; apply/(fh _ (to_set ((_^-1)%classic) _)). exact: nbhs_entourage (entourage_inv _). apply: (entourage_split (g x2)) => //; move: (x2); [near: x1|near: y1]. have /cvg_fct_entourageP /(_ (_^-1)%classic) := fg; apply. exact: entourage_inv. by have /cvg_fct_entourageP := fg; apply. 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