proposition: Lemma open_subball {R : realFieldType} {M : normedModType R} (A : set M) (x : M) : open A -> A x -> \forall e \near 0^'+, ball x e `<=` A.
proof: Proof. move=> aA Ax. have /(@nbhs_closedballP R M _ x)[r xrA]: nbhs x A by rewrite nbhsE/=; exists A. near=> e. apply/(subset_trans _ xrA)/(subset_trans _ (@subset_closed_ball _ _ _ _)) => //. by apply: le_ball; near: e; apply: nbhs_right_le. 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