proposition: Lemma subspace_pm_entourageE : @entourage (subspace A) = entourage_ subspace_ball.
proof: Proof. rewrite eqEsubset; split; rewrite /subspace_ball. move=> U [W + subU]; rewrite -entourage_ballE => [[eps] nneg subW]. exists eps => //; apply: (subset_trans _ subU). move=> [x y] /=; case: ifP => /asboolP ?. by move=> [Ay xBy]; right; repeat split => //; exact: subW. by move=> ->; left. move=> E [eps nneg subE]; exists [set xy | ball (xy.1 : X) eps xy.2]. by rewrite -entourage_ballE; exists eps. move=> [x y] /= [->|[]Ax []Ay xBy]; apply: subE => //=. by case: ifP => /asboolP; split => //; exact: ballxx. by case: ifP => /asboolP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed