proposition: Lemma ereal_inf_pinfty S : ereal_inf S = +oo <-> S `<=` [set +oo].
proof: Proof. rewrite eqe_oppLRP oppe_subset image_set1; exact: ereal_sup_ninfty. 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