proposition: Lemma closed_ballE (R : realFieldType) (V : normedModType R) (x : V) (r : R) : 0 < r -> closed_ball x r = closed_ball_ normr x r.
proof: Proof. move=> /posnumP[e]; rewrite eqEsubset; split => y. rewrite /closed_ball closureE; apply; split; first exact: closed_closed_ball_. by move=> z; rewrite -ball_normE; exact: ltW. have [-> _|xy] := eqVneq x y; first exact: closed_ballxx. rewrite /closed_ball closureE -ball_normE. rewrite /closed_ball_ /= le_eqVlt. move => /orP[/eqP xye B [Bc Be]|xye _ [_ /(_ _ xye)]//]. apply: Bc => B0 /nbhs_ballP[s s0] B0y. have [es|se] := leP s e%:num; last first. exists x; split; first by apply: Be; rewrite ball_normE; apply: ballxx. by apply: B0y; rewrite -ball_normE /ball_ /= distrC xye. exists (y + (s / 2) *: (`|x - y|^-1 *: (x - y))); split; [apply: Be|apply: B0y]. rewrite /= opprD addrA -[X in `|X - _|](scale1r (x - y)) scalerA -scalerBl. rewrite -[X in X - _](@divrr _ `|x - y|) ?unitfE ?normr_eq0 ?subr_eq0//. rewrite -mulrBl -scalerA normrZ normfZV ?subr_eq0// mulr1. rewrite gtr0_norm; first by rewrite ltrBlDl xye ltrDr mulr_gt0. by rewrite subr_gt0 xye ltr_pdivrMr // mulr_natr mulr2n ltr_pwDl. rewrite -ball_normE /ball_ /= opprD addrA addrN add0r normrN normrZ. rewrite normfZV ?subr_eq0// mulr1 normrM (gtr0_norm s0) gtr0_norm //. by rewrite ltr_pdivrMr // ltr_pMr // ltr1n. 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