proposition: Lemma countable_uniformityP {T : uniformType} : countable_uniformity T <-> exists2 f : nat -> set (T * T), (forall A, entourage A -> exists N, f N `<=` A) & (forall n, entourage (f n)).
proof: Proof. split=> [[M []]|[f fsubE entf]]. move=> /pfcard_geP[-> _ /(_ _ entourageT)[]//|/unsquash f eM Msub]. exists f; last by move=> n; apply: eM; exact: funS. by move=> ? /Msub [Q + ?] => /(@surj _ _ _ _ f)[n _ fQ]; exists n; rewrite fQ. exists (range f); split; first exact: card_image_le. by move=> E [n _] <-; exact: entf. by move=> E /fsubE [n fnA]; exists (f n) => //; exists n. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed