proposition: Lemma edist_inf_continuous : continuous edist_inf.
proof: Proof. move=> z; have [A0|/= /set0P[a0 Aa0]] := eqVneq A set0. rewrite /edist_inf A0. under eq_fun do rewrite image_set0 ereal_inf0. exact: cvg_cst. have [] := eqVneq (edist_inf z) +oo%E. move=> /[dup] fzp /ereal_inf_pinfty => zAp U /= Ufz. have : nbhs z (ball z 1) by exact: nbhsx_ballx. apply: filter_app; near_simpl; near=> w => bz1w. suff /= -> : (edist_inf w) = +oo%E by apply: nbhs_singleton; rewrite -fzp. apply/ereal_inf_pinfty => r [a Aa] war; apply/zAp; exists a => //. have /gee0P[|[r' r'pos war']] := edist_ge0 (w, a). by rewrite war => ->; apply: zAp; exists a. have := @edist_triangle _ _ z w a; rewrite war'; apply: contra_leP => _. rewrite (@le_lt_trans _ _ (1 + r'%:E)%E) ?leeD2r ?edist_fin//. by rewrite -EFinD [edist (z, a)]zAp ?ltey //; exists a. rewrite -ltey -ge0_fin_numE ?edist_inf_ge0 // => fz_fin. rewrite /continuous_at -[edist_inf z]fineK //; apply/fine_cvgP. have fwfin : \forall w \near z, edist_inf w \is a fin_num. (have : nbhs z (ball z 1) by exact: nbhsx_ballx); apply: filter_app. near=> t => bz1; rewrite ge0_fin_numE ?edist_inf_ge0 //. rewrite (le_lt_trans (edist_inf_triangle _ z))//. rewrite -ge0_fin_numE ?adde_ge0 ?edist_inf_ge0 //. rewrite fin_numD fz_fin andbT; apply/edist_finP; exists 1 => //. exact/ball_sym. split => //; apply/cvgrPdist_le => _/posnumP[eps]. have : nbhs z (ball z eps%:num) by exact: nbhsx_ballx. apply: filter_app; near_simpl; move: fwfin; apply: filter_app. near=> t => tfin /= /[dup] ?. have ztfin : edist (z, t) \is a fin_num by apply/edist_finP; exists eps%:num. move=> /(@edist_fin _ _ _ (z, t)) - /(_ trivial). rewrite -[edist (z, t)]fineK ?lee_fin //; apply: le_trans. rewrite ler_norml; apply/andP; split. rewrite lerBrDr addrC lerBlDr addrC -fineD //. rewrite -lee_fin ?fineK // ?fin_numD ?ztfin ?fz_fin // edist_sym. exact: edist_inf_triangle. rewrite lerBlDr -fineD // -lee_fin ?fineK // ?fin_numD ?tfin ?ztfin //. exact: edist_inf_triangle. Unshelve. all: by 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