proposition: Lemma uniform_pseudometric_sup {R : realType} {T : uniformType} : @entourage T = @sup_ent T {E : set (T * T) | @entourage T E} (fun E => Uniform.class (@gauge.type T (projT1 E) (projT2 E))).
proof: Proof. rewrite eqEsubset; split => [E entE|E]. exists E => //=. pose pe : {classic {E0 : set (T * T) | _}} * _ := (exist _ E entE, E). have entPE : `[< @entourage (gauge.type entE) E >]. by apply/asboolP; exists 0%N => // ? []. exists (fset1 (exist _ pe entPE)) => //=; first by move=> ?; rewrite in_setE. by rewrite set_fset1 bigcap_set1. case=> W /= [/= J] _ <- /filterS; apply; apply: filter_bigI => -[] [] [] /= D. move=> entD G /[dup] /asboolP [n _ + _ _] => /filterS; apply. exact: gauge.iter_split_ent. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed