proposition: Lemma mx_entourage : entourage = entourage_ mx_ball.
proof: Proof. rewrite predeqE=> A; split; last first. move=> [_/posnumP[e] sbeA]. by exists (fun _ _ => [set xy | ball xy.1 e%:num xy.2]). move=> [P]; rewrite -entourage_ballE => entP sPA. set diag := fun (e : {posnum R}) => [set xy : T * T | ball xy.1 e%:num xy.2]. exists (\big[Num.min/1%:pos]_i \big[Num.min/1%:pos]_j xget 1%:pos (fun e : {posnum R} => diag e `<=` P i j))%:num => //=. move=> MN MN_min; apply: sPA => i j. have /(xgetPex 1%:pos): exists e : {posnum R}, diag e `<=` P i j. by have [_/posnumP[e]] := entP i j; exists e. apply; apply: le_ball (MN_min i j). apply: le_trans (@bigmin_le _ [the orderType _ of {posnum R}] _ _ i _) _. exact: bigmin_le. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed