proposition: Lemma weak_pseudo_metric_entourageE : entourage = entourage_ weak_ball.
proof: Proof. rewrite /entourage /= /weak_ent -entourage_ballE /entourage_. have -> : (fun e => [set xy | ball (f xy.1) e (f xy.2)]) = (preimage (map_pair f) \o fun e => [set xy | ball xy.1 e xy.2])%FUN. by []. rewrite eqEsubset; split; apply/filter_fromP. - apply: filter_from_filter; first by exists 1 => /=. move=> e1 e2 e1pos e2pos; wlog e1lee2 : e1 e2 e1pos e2pos / e1 <= e2. by have [?|/ltW ?] := lerP e1 e2; [exact | rewrite setIC; exact]. exists e1 => //; rewrite -preimage_setI; apply: preimage_subset. by move=> ? ?; split => //; apply: le_ball; first exact: e1lee2. - by move=> E [e ?] heE; exists e => //; apply: preimage_subset. - apply: filter_from_filter. by exists [set xy | (ball xy.1 1 xy.2)]; exists 1 => /=. move=> E1 E2 [e1 e1pos he1E1] [e2 e2pos he2E2]. wlog ? : E1 E2 e1 e2 e1pos e2pos he1E1 he2E2 / e1 <= e2. have [? /(_ _ _ e1 e2)|/ltW ? ] := lerP e1 e2; first exact. by rewrite setIC => /(_ _ _ e2 e1); exact. exists (E1 `&` E2) => //; exists e1 => // xy /= B; split; first exact: he1E1. by apply/he2E2/le_ball; last exact: B. - by move=> e ?; exists ([set xy | ball xy.1 e xy.2]) => //; by exists e => /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed