proposition: Lemma interior_closed_ballE (R : realType) (V : normedModType R) (x : V) (r : R) : 0 < r -> (closed_ball x r)^° = ball x r.
proof: Proof. move=> r0; rewrite eqEsubset; split; last first. by rewrite -open_subsetE; [exact: subset_closure | exact: ball_open]. move=> /= t; rewrite closed_ballE // /interior /= -nbhs_ballE => [[]] s s0. have [-> _|nxt] := eqVneq t x; first exact: ballxx. near ((0 : R^o)^') => e; rewrite -ball_normE /closed_ball_ => tsxr. pose z := t + `|e| *: (t - x); have /tsxr /= : `|t - z| < s. rewrite distrC addrAC subrr add0r normrZ normr_id. rewrite -ltr_pdivlMr ?(normr_gt0,subr_eq0) //. by near: e; apply/dnbhs0_lt; rewrite divr_gt0 // normr_gt0 subr_eq0. rewrite /z opprD addrA -scalerN -{1}(scale1r (x - t)) opprB -scalerDl normrZ. apply lt_le_trans; rewrite ltr_pMl; last by rewrite normr_gt0 subr_eq0 eq_sym. by rewrite ger0_norm // ltrDl normr_gt0; near: e; exists 1 => /=. 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