proposition: Lemma compact_cauchy_cvg {T : uniformType} (U : set T) (F : set_system T) : ProperFilter F -> cauchy F -> F U -> compact U -> cvg F.
proof: Proof. move=> PF cf FU /(_ F PF FU) [x [_ clFx]]; apply: (cvgP x). apply/cvg_entourageP => E entE. have : nbhs entourage (split_ent E) by rewrite nbhs_filterE. move=> /(cf (split_ent E))[] [D1 D2]/= /[!nbhs_simpl] -[FD1 FD2 D1D2E]. have : nbhs x to_set (split_ent E) x by exact: nbhs_entourage. move=> /(clFx _ (to_set (split_ent E) x) FD1)[z [Dz Exz]]. by near=> t; apply/(entourage_split z entE Exz)/D1D2E; split => //; near: t. 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