proposition: Lemma nbhs_image_EFin (x : R) (X : set R) : nbhs x X -> nbhs x%:E ((fun r => r%:E) @` X).
proof: Proof. case => _/posnumP[e] xeX; exists e%:num => //= r xer. by exists r => //; apply xeX. 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