proposition: Lemma edist_closeP x y : close x y <-> edist (x, y) = 0%E.
proof: Proof. rewrite ball_close; split=> [bxy|edist0 eps]; first last. by apply: (@edist_lt_ball _ (x, y)); rewrite edist0. case: ltgtP (edist_ge0 (x, y)) => // dpos _. have xxfin : edist (x, y) \is a fin_num. by rewrite ge0_fin_numE// (@le_lt_trans _ _ 1%:E) ?ltey// edist_fin. have dpose : fine (edist (x, y)) > 0 by rewrite -lte_fin fineK. pose eps := PosNum dpose. have : (edist (x, y) <= (eps%:num / 2)%:E)%E. apply: ereal_inf_lb; exists (eps%:num / 2) => //; split => //. exact: (bxy (eps%:num / 2)%:pos). apply: contra_leP => _. by rewrite /= EFinM fineK// lte_pdivr_mulr// lte_pmulr// lte1n. 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