proposition: Lemma closure_sup (R : realType) (A : set R) : A !=set0 -> has_ubound A -> closure A (sup A).
proof: Proof. move=> A0 ?; have [|AsupA] := pselect (A (sup A)); first exact: subset_closure. rewrite closure_limit_point; right => U /nbhs_ballP[_ /posnumP[e]] supAeU. suff [x [Ax /andP[sAex xsA]]] : exists x, A x /\ sup A - e%:num < x < sup A. exists x; split => //; first by rewrite lt_eqF. apply supAeU; rewrite /ball /= ltr_distl (addrC x e%:num) -ltrBlDl sAex. by rewrite andbT (le_lt_trans _ xsA) // lerBlDl lerDr. apply: contrapT => /forallNP Ax. suff /(sup_le_ub A0) : ubound A (sup A - e%:num). by rewrite leNgt => /negP; apply; rewrite ltrBlDl ltrDr. move=> y Ay; have /not_andP[//|/negP] := Ax y. rewrite negb_and leNgt => /orP[//|]; apply: contra => sAey. rewrite lt_neqAle sup_upper_bound // andbT. by apply: contra_not_neq AsupA => <-. 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