proposition: Lemma open_itvoo_subset : open A -> A x -> \forall r \near 0^'+, `]x - r, x + r[ `<=` A.
proof: Proof. move=> /[apply] -[] _/posnumP[r] /subset_ball_prop_in_itv xrA. exists r%:num => //= k; rewrite /= distrC subr0 set_itvoo => /ltr_normlW kr k0. by apply/(subset_trans _ xrA)/subset_itvW; [rewrite lerB//; exact: ltW | rewrite lerD//; exact: ltW]. 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