proposition: Lemma ereal_sup_EFin (A : set R) : has_ubound A -> A !=set0 -> ereal_sup (EFin @` A) = (sup A)%:E.
proof: Proof. move=> has_ubA A0; apply/eqP; rewrite eq_le; apply/andP; split. by apply: ub_ereal_sup => /= y [r Ar <-{y}]; rewrite lee_fin sup_ub. set esup := ereal_sup _; have := leey esup. rewrite le_eqVlt => /predU1P[->|esupoo]; first by rewrite leey. have := leNye esup; rewrite le_eqVlt => /predU1P[/esym|ooesup]. case: A0 => i Ai. by move=> /ereal_sup_ninfty /(_ i%:E) /(_ (ex_intro2 A _ i Ai erefl)). have esup_fin_num : esup \is a fin_num. by rewrite fin_numE -leeNy_eq -ltNge ooesup /= -leye_eq -ltNge esupoo. rewrite -(@fineK _ esup) // lee_fin leNgt. apply/negP => /(sup_gt A0)[r Ar]; apply/negP; rewrite -leNgt. by rewrite -lee_fin fineK//; apply: ereal_sup_ub; exists r. 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