proposition: Lemma closed_closed_ball_ (R : realFieldType) (V : normedModType R) (x : V) (e : R) : closed (closed_ball_ normr x e).
proof: Proof. rewrite /closed_ball_ -/((normr \o (fun y => x - y)) @^-1` [set x | x <= e]). apply: (closed_comp _ (@closed_le _ _)) => y _. apply: (continuous_comp _ (@norm_continuous _ _ _)). exact: (continuousB (@cst_continuous _ _ _ _)). 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