proposition: Lemma countable_uniformity_metric {R : realType} {T : pseudoMetricType R} : countable_uniformity T.
proof: Proof. apply/countable_uniformityP. exists (fun n => [set xy : T * T | ball xy.1 n.+1%:R^-1 xy.2]); last first. by move=> n; exact: (entourage_ball _ n.+1%:R^-1%:pos). move=> E; rewrite -entourage_ballE => -[e e0 subE]. exists `|floor e^-1|%N; apply: subset_trans subE => xy; apply: le_ball. rewrite /= -[leRHS]invrK lef_pV2 ?posrE ?invr_gt0// -natr1. by rewrite natr_absz ger0_norm ?floor_ge0 ?invr_ge0// 1?ltW// lt_succ_floor. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed