proposition: Lemma ereal_inf_EFin (A : set R) : has_lbound A -> A !=set0 -> ereal_inf (EFin @` A) = (inf A)%:E.
proof: Proof. move=> has_lbA A0; rewrite /ereal_inf /inf EFinN; congr (- _)%E. rewrite -ereal_sup_EFin; [|exact/has_lb_ubN|exact/nonemptyN]. by rewrite !image_comp. 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