proposition: Lemma supremumsT : supremums [set: \bar R] = [set +oo].
proof: Proof. rewrite /supremums uboundT. by apply/seteqP; split=> [x []//|x -> /=]; split => // y ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal