proposition: Lemma edist_continuous : continuous edist.
proof: Proof. move=> [x y]; have [pE U /= Upinf|] := eqVneq (edist (x, y)) +oo%E. rewrite nbhs_simpl /=; apply (@filterS _ _ _ [set xy | edist xy = +oo]%E). by move=> z /= ->; apply: nbhs_singleton; move: pE Upinf => ->. by apply: open_nbhs_nbhs; split => //; exact: edist_pinfty_open. rewrite -ltey -ge0_fin_numE// => efin. rewrite /continuous_at -[edist (x, y)]fineK//; apply: cvg_EFin. by have := edist_fin_open efin; apply: filter_app; near=> w. apply/cvgrPdist_le => _/posnumP[eps]. suff: \forall t \near (nbhs x, nbhs y), `|fine (edist (x, y)) - fine (edist t)| <= eps%:num by []. rewrite -near2_pair; near=> a b => /=. have abxy : (edist (a, b) <= edist (x, a) + edist (x, y) + edist (y, b))%E. rewrite (edist_sym x a) -addeA. by rewrite (le_trans (@edist_triangle _ x _)) ?leeD ?edist_triangle. have xyab : (edist (x, y) <= edist (x, a) + edist (a, b) + edist (y, b))%E. rewrite (edist_sym y b) -addeA. by rewrite (le_trans (@edist_triangle _ a _))// ?leeD// ?edist_triangle. have xafin : edist (x, a) \is a fin_num. by apply/edist_finP; exists 1 =>//; near: a; exact: nbhsx_ballx. have ybfin : edist (y, b) \is a fin_num. by apply/edist_finP; exists 1 =>//; near: b; exact: nbhsx_ballx. have abfin : edist (a, b) \is a fin_num. by rewrite ge0_fin_numE// (le_lt_trans abxy) ?lte_add_pinfty// -ge0_fin_numE. have xyabfin: (edist (x, y) - edist (a, b))%E \is a fin_num by rewrite fin_numB abfin efin. rewrite -fineB// -fine_abse// -lee_fin fineK ?abse_fin_num//. rewrite (@le_trans _ _ (edist (x, a) + edist (y, b))%E)//; last first. by rewrite [eps%:num]splitr/= EFinD leeD//; apply: edist_fin => //=; [near: a | near: b]; exact: nbhsx_ballx. have [ab_le_xy|/ltW xy_le_ab] := leP (edist (a, b)) (edist (x, y)). by rewrite gee0_abs ?subre_ge0// lee_subl_addr// addeAC. rewrite lee0_abs ?sube_le0// oppeB ?fin_num_adde_defr//. by rewrite addeC lee_subl_addr// addeAC. Unshelve. all: end_near. 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