proposition: Lemma open_bigcup_rat U : open U -> U = \bigcup_(q in [set q | ratr q \in U]) bigcup_ointsub U q.
proof: Proof. move=> oU; have [->|U0] := eqVneq U set0. by rewrite bigcup0// => q _; rewrite bigcup_ointsub0. apply/seteqP; split=> [x Ux|x [p _ Ipx]]; last exact: bigcup_ointsub_sub Ipx. suff [q Iqx] : exists q, bigcup_ointsub U q x. by exists q => //=; rewrite in_setE; case: Iqx => A [[_ _ +] ? _]; exact. have : nbhs x U by rewrite nbhsE /=; exists U. rewrite -nbhs_ballE /nbhs_ball /nbhs_ball_ => -[_/posnumP[r] xrU]. have /rat_in_itvoo[q qxxr] : (x - r%:num < x + r%:num)%R. by rewrite ltrBlDr -addrA ltrDl. exists q, `](x - r%:num)%R, (x + r%:num)%R[%classic; last first. by rewrite /= in_itv/= ltrBlDl ltrDr// ltrDl//; apply/andP. split=> //; split; [exact: interval_open|exact: interval_is_interval|]. move=> y /=; rewrite in_itv/= => /andP[xy yxr]; apply xrU => /=. rewrite /ball /= /ball_ /= in xrU *; have [yx|yx] := leP x y. by rewrite ler0_norm ?subr_le0// opprB ltrBlDl. by rewrite gtr0_norm ?subr_gt0// ltrBlDr -ltrBlDl. 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