proposition: Lemma close_cvg (F1 F2 : set_system T) {FF2 : ProperFilter F2} : F1 --> F2 -> F2 --> F1 -> close (lim F1) (lim F2).
proof: Proof. move=> F12 F21. have [/(cvg_trans F21) F2l|dvgF1] := pselect (cvg F1). by apply: (@cvg_close F2) => //; apply: cvgP F2l. have [/(cvg_trans F12)/cvgP//|dvgF2] := pselect (cvg F2). rewrite dvgP // dvgP //; exact/close_refl. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed