proposition: Lemma cvg_switch {U : completeType} F1 (FF1 : ProperFilter F1) F2 (FF2 : ProperFilter F2) (f : T1 -> T2 -> U) (g : T2 -> U) (h : T1 -> U) : f @ F1 --> g -> (forall x1, f x1 @ F2 --> h x1) -> exists l : U, h @ F1 --> l /\ g @ F2 --> l.
proof: Proof. move=> Hfg Hfh; have hcv := !! cvg_switch_2 Hfg Hfh. by exists (lim (h @ F1)); split=> //; apply: cvg_switch_1 Hfg Hfh hcv. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed