proposition: Lemma left_bounded_interior (R : realType) (X : set R) : has_lbound X -> X^° `<=` [set r | inf X < r].
proof: Proof. move=> lX r Xr; rewrite /mkset ltNge; apply/negP. rewrite le_eqVlt => /orP[/eqP rinfX|]; last first. by apply/negP; rewrite -leNgt inf_lb //; exact: interior_subset. suff : ~ X^° (inf X) by rewrite -rinfX. case/nbhs_ballP => _/posnumP[e] supXeX. have [f XsupXf] : exists f : {posnum R}, X (inf X - f%:num). exists (e%:num / 2)%:pos; apply supXeX; rewrite /ball /= opprB addrCA subrr. by rewrite addr0 gtr0_norm // ltr_pdivrMr // ltr_pMr // ltr1n. have : inf X <= inf X - f%:num by apply inf_lb. by apply/negP; rewrite -ltNge; rewrite ltrBlDr ltrDl. 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