proposition: Lemma edist_pinftyP (xy : X * X) : (edist xy = +oo)%E <-> (forall r, 0 < r -> ~ ball xy.1 r xy.2).
proof: Proof. split. move/ereal_inf_pinfty => xrb r rpos rb; move: (ltry r); rewrite ltey => /eqP. by apply; apply: xrb; exists r. rewrite /edist=> nrb; suff -> : [set r | 0 < r /\ ball xy.1 r xy.2] = set0. by rewrite image_set0 ereal_inf0. by rewrite -subset0 => r [?] rb; apply: nrb; last exact: rb. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule